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  5344  relsnb  5756  ffdm  6699  ov  7513  ovg  7534  oacl  8476  nnacl  8552  elpm2r  8795  djuxpdom  10115  djufi  10116  cfcof  10203  hargch  10602  uzaddcl  12839  expcllem  14013  lcmfval  16567  lcmf0val  16568  mreunirn  17538  filunirn  23745  ustelimasn  24086  metustfbas  24421  zrtelqelz  26644  usgreqdrusgr  29472  pjini  31601  fzspl  32685  f1ocnt  32698  xrge0tsmsbi  32976  bnj983  34914  poimirlem16  37603  poimirlem19  37606  poimirlem25  37612  ac6s6  38139  fouriersw  46202  etransclem25  46230  ismea  46422  bits0oALTV  47655  uzlidlring  48196  linccl  48376  resinsnlem  48832  isinito2  49461  termc2  49480  discsntermlem  49532