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  5359  relsnb  5783  ffdm  6732  ov  7557  ovg  7578  oacl  8522  nnacl  8599  elpm2r  8844  djuxpdom  10188  djufi  10189  cfcof  10276  hargch  10682  uzaddcl  12953  expcllem  14136  lcmfval  16711  lcmf0val  16712  mreunirn  17685  filunirn  24108  ustelimasn  24449  metustfbas  24783  zrtelqelz  26995  usgreqdrusgr  30028  pjini  32180  fzspl  33260  f1ocnt  33271  xrge0tsmsbi  33514  bnj983  35460  kardenir  35684  kardnnfi  35695  poimirlem16  38385  poimirlem19  38388  poimirlem25  38394  ac6s6  38920  fouriersw  47059  etransclem25  47087  ismea  47279  bits0oALTV  48597  uzlidlring  49150  linccl  49344  resinsnlem  49797  isinito2  50425  termc2  50444  discsntermlem  50496