Theorem ibir 256

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 212	. 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
3	2	ibi 255	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 195

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 196

This theorem is referenced by:  elpr2OLD  4148  eusv2i  4789  ffdm  5975  ov  6678  ovg  6697  oacl  7502  nnacl  7578  elpm2r  7761  cdaxpdom  8894  cdafi  8895  cfcof  8979  hargch  9374  uzaddcl  11620  expcllem  12733  lcmfval  15172  lcmf0val  15173  mreunirn  16084  filunirn  21496  ustelimasn  21836  metustfbas  22172  pjini  27942  fzspl  28938  f1ocnt  28946  xrge0tsmsbi  29117  bnj983  30275  poimirlem16  32595  poimirlem19  32598  poimirlem25  32604  ac6s6  33150  fouriersw  39124  etransclem25  39152  bits0oALTV  40130  usgreqdrusgr  40768  uzlidlring  41719  linccl  41997