Theorem ibir 257

Description: Inference that converts a biconditional implied by one of its arguments, into an implication. (Contributed by NM, 22-Jul-2004.)

Hypothesis

Ref	Expression
ibir.1	⊢ (𝜑 → (𝜓 ↔ 𝜑))

Assertion

Ref	Expression
ibir	⊢ (𝜑 → 𝜓)

Proof of Theorem ibir

Step	Hyp	Ref	Expression
1		ibir.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜑))
2	1	bicomd 213	. 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
3	2	ibi 256	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 196

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 197

This theorem is referenced by:  elpr2OLD  4337  eusv2i  5004  ffdm  6215  ov  6937  ovg  6956  oacl  7776  nnacl  7852  elpm2r  8033  cdaxpdom  9195  cdafi  9196  cfcof  9280  hargch  9679  uzaddcl  11929  expcllem  13057  lcmfval  15528  lcmf0val  15529  mreunirn  16455  filunirn  21879  ustelimasn  22219  metustfbas  22555  usgreqdrusgr  26666  pjini  28859  fzspl  29851  f1ocnt  29860  xrge0tsmsbi  30087  bnj983  31320  poimirlem16  33730  poimirlem19  33733  poimirlem25  33739  ac6s6  34285  fouriersw  40943  etransclem25  40971  bits0oALTV  42094  uzlidlring  42431  linccl  42705