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  1097  eusv2i  5363  relsnb  5787  ffdm  6733  ov  7552  ovg  7573  oacl  8516  nnacl  8593  elpm2r  8838  djuxpdom  10165  djufi  10166  cfcof  10254  hargch  10654  uzaddcl  12924  expcllem  14104  lcmfval  16675  lcmf0val  16676  mreunirn  17649  filunirn  24004  ustelimasn  24345  metustfbas  24679  zrtelqelz  26885  usgreqdrusgr  29855  pjini  31988  fzspl  33071  f1ocnt  33082  xrge0tsmsbi  33331  bnj983  35280  poimirlem16  38170  poimirlem19  38173  poimirlem25  38179  ac6s6  38706  fouriersw  46832  etransclem25  46860  ismea  47052  bits0oALTV  48330  uzlidlring  48884  linccl  49074  resinsnlem  49529  isinito2  50157  termc2  50176  discsntermlem  50228