Theorem ibir 269

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

Syntax hints:   → wi 4   ↔ wb 207

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 208

This theorem is referenced by:  elimh  1088  eusv2i  5323  relsnb  5745  ffdm  6684  ov  7500  ovg  7521  oacl  8460  nnacl  8537  elpm2r  8782  djuxpdom  10099  djufi  10100  cfcof  10187  hargch  10587  uzaddcl  12845  expcllem  14025  lcmfval  16581  lcmf0val  16582  mreunirn  17554  filunirn  23865  ustelimasn  24206  metustfbas  24540  zrtelqelz  26740  usgreqdrusgr  29655  pjini  31788  fzspl  32881  f1ocnt  32892  xrge0tsmsbi  33155  bnj983  35133  poimirlem16  38003  poimirlem19  38006  poimirlem25  38012  ac6s6  38539  fouriersw  46674  etransclem25  46702  ismea  46894  bits0oALTV  48172  uzlidlring  48726  linccl  48905  resinsnlem  49361  isinito2  49989  termc2  50008  discsntermlem  50060