Theorem ibir 268

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 223	. 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
3	2	ibi 267	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 206

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 207

This theorem is referenced by:  elimh  1083  eusv2i  5331  relsnb  5751  ffdm  6691  ov  7504  ovg  7525  oacl  8463  nnacl  8540  elpm2r  8785  djuxpdom  10099  djufi  10100  cfcof  10187  hargch  10587  uzaddcl  12845  expcllem  14025  lcmfval  16581  lcmf0val  16582  mreunirn  17554  filunirn  23857  ustelimasn  24198  metustfbas  24532  zrtelqelz  26735  usgreqdrusgr  29652  pjini  31785  fzspl  32877  f1ocnt  32888  xrge0tsmsbi  33150  bnj983  35109  poimirlem16  37971  poimirlem19  37974  poimirlem25  37980  ac6s6  38507  fouriersw  46677  etransclem25  46705  ismea  46897  bits0oALTV  48169  uzlidlring  48723  linccl  48902  resinsnlem  49358  isinito2  49986  termc2  50005  discsntermlem  50057