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

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  elimh  1082  eusv2i  5339  relsnb  5751  ffdm  6691  ov  7502  ovg  7523  oacl  8462  nnacl  8539  elpm2r  8782  djuxpdom  10096  djufi  10097  cfcof  10184  hargch  10584  uzaddcl  12817  expcllem  13995  lcmfval  16548  lcmf0val  16549  mreunirn  17520  filunirn  23826  ustelimasn  24167  metustfbas  24501  zrtelqelz  26724  usgreqdrusgr  29642  pjini  31774  fzspl  32869  f1ocnt  32880  xrge0tsmsbi  33156  bnj983  35107  poimirlem16  37837  poimirlem19  37840  poimirlem25  37846  ac6s6  38373  fouriersw  46475  etransclem25  46503  ismea  46695  bits0oALTV  47927  uzlidlring  48481  linccl  48660  resinsnlem  49116  isinito2  49744  termc2  49763  discsntermlem  49815