Theorem ibir 271

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  elimh  1085  eusv2i  5272  relsnb  5657  ffdm  6553  ov  7331  ovg  7351  oacl  8240  nnacl  8317  elpm2r  8504  djuxpdom  9764  djufi  9765  cfcof  9853  hargch  10252  uzaddcl  12465  expcllem  13611  lcmfval  16141  lcmf0val  16142  mreunirn  17058  filunirn  22733  ustelimasn  23074  metustfbas  23409  usgreqdrusgr  27610  pjini  29734  fzspl  30785  f1ocnt  30797  xrge0tsmsbi  30991  bnj983  32598  poimirlem16  35479  poimirlem19  35482  poimirlem25  35488  ac6s6  36016  zrtelqelz  39994  fouriersw  43390  etransclem25  43418  ismea  43607  bits0oALTV  44749  uzlidlring  45103  linccl  45371