Theorem ibir 267

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 266	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  1082  eusv2i  5321  relsnb  5710  ffdm  6627  ov  7409  ovg  7429  oacl  8348  nnacl  8425  elpm2r  8614  djuxpdom  9940  djufi  9941  cfcof  10029  hargch  10428  uzaddcl  12641  expcllem  13789  lcmfval  16322  lcmf0val  16323  mreunirn  17306  filunirn  23029  ustelimasn  23370  metustfbas  23709  usgreqdrusgr  27931  pjini  30055  fzspl  31105  f1ocnt  31117  xrge0tsmsbi  31312  bnj983  32925  poimirlem16  35787  poimirlem19  35790  poimirlem25  35796  ac6s6  36324  zrtelqelz  40340  fouriersw  43741  etransclem25  43769  ismea  43958  bits0oALTV  45100  uzlidlring  45454  linccl  45722