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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  elimh  1099  eusv2i  5355  relsnb  5780  ffdm  6742  ov  7566  ovg  7587  oacl  8548  nnacl  8625  elpm2r  8870  djuxpdom  10269  djufi  10270  cfcof  10357  hargch  10763  uzaddcl  13036  expcllem  14220  lcmfval  16803  lcmf0val  16804  mreunirn  17778  filunirn  24208  ustelimasn  24549  metustfbas  24883  zrtelqelz  27093  usgreqdrusgr  30156  pjini  32308  fzspl  33429  f1ocnt  33440  xrge0tsmsbi  33683  bnj983  35629  kardenir  35884  kardnnfi  35895  j0ltaleph  35949  poimirlem16  38661  poimirlem19  38664  poimirlem25  38670  ac6s6  39211  fouriersw  47348  etransclem25  47376  ismea  47568  bits0oALTV  48886  uzlidlring  49439  linccl  49633  resinsnlem  50091  isinito2  50741  termc2  50760  discsntermlem  50815