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  5367  relsnb  5791  ffdm  6739  ov  7560  ovg  7581  oacl  8522  nnacl  8599  elpm2r  8844  djuxpdom  10181  djufi  10182  cfcof  10269  hargch  10669  uzaddcl  12940  expcllem  14122  lcmfval  16697  lcmf0val  16698  mreunirn  17671  filunirn  24070  ustelimasn  24411  metustfbas  24745  zrtelqelz  26954  usgreqdrusgr  29952  pjini  32098  fzspl  33180  f1ocnt  33191  xrge0tsmsbi  33434  bnj983  35380  kardenir  35604  kardnnfi  35615  poimirlem16  38320  poimirlem19  38323  poimirlem25  38329  ac6s6  38854  fouriersw  46978  etransclem25  47006  ismea  47198  bits0oALTV  48479  uzlidlring  49033  linccl  49227  resinsnlem  49682  isinito2  50310  termc2  50329  discsntermlem  50381