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  5363  relsnb  5789  ffdm  6769  ov  7596  ovg  7617  oacl  8581  nnacl  8658  elpm2r  8903  djuxpdom  10303  djufi  10304  cfcof  10391  hargch  10797  uzaddcl  13071  expcllem  14255  lcmfval  16840  lcmf0val  16841  mreunirn  17821  filunirn  24256  ustelimasn  24597  metustfbas  24931  zrtelqelz  27143  usgreqdrusgr  30206  pjini  32358  fzspl  33477  f1ocnt  33488  xrge0tsmsbi  33734  bnj983  35692  kardenir  35967  kardnnfi  35978  j0ltaleph  36049  poimirlem16  38822  poimirlem19  38825  poimirlem25  38831  ac6s6  39370  fouriersw  47514  etransclem25  47542  ismea  47734  bits0oALTV  49052  uzlidlring  49605  linccl  49857  resinsnlem  50315  isinito2  50965  termc2  50984  discsntermlem  51039