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  5317  relsnb  5712  ffdm  6630  ov  7417  ovg  7437  oacl  8365  nnacl  8442  elpm2r  8633  djuxpdom  9941  djufi  9942  cfcof  10030  hargch  10429  uzaddcl  12644  expcllem  13793  lcmfval  16326  lcmf0val  16327  mreunirn  17310  filunirn  23033  ustelimasn  23374  metustfbas  23713  usgreqdrusgr  27935  pjini  30061  fzspl  31111  f1ocnt  31123  xrge0tsmsbi  31318  bnj983  32931  poimirlem16  35793  poimirlem19  35796  poimirlem25  35802  ac6s6  36330  zrtelqelz  40345  fouriersw  43772  etransclem25  43800  ismea  43989  bits0oALTV  45133  uzlidlring  45487  linccl  45755