Theorem ibir 268

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  elimh  1084  eusv2i  5393  relsnb  5803  ffdm  6748  ov  7552  ovg  7572  oacl  8535  nnacl  8611  elpm2r  8839  djuxpdom  10180  djufi  10181  cfcof  10269  hargch  10668  uzaddcl  12888  expcllem  14038  lcmfval  16558  lcmf0val  16559  mreunirn  17545  filunirn  23386  ustelimasn  23727  metustfbas  24066  usgreqdrusgr  28825  pjini  30952  fzspl  32001  f1ocnt  32013  xrge0tsmsbi  32210  bnj983  33962  poimirlem16  36504  poimirlem19  36507  poimirlem25  36513  ac6s6  37040  zrtelqelz  41235  fouriersw  44947  etransclem25  44975  ismea  45167  bits0oALTV  46349  uzlidlring  46827  linccl  47095