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  1082  eusv2i  5349  relsnb  5765  ffdm  6717  ov  7533  ovg  7554  oacl  8499  nnacl  8575  elpm2r  8818  djuxpdom  10139  djufi  10140  cfcof  10227  hargch  10626  uzaddcl  12863  expcllem  14037  lcmfval  16591  lcmf0val  16592  mreunirn  17562  filunirn  23769  ustelimasn  24110  metustfbas  24445  zrtelqelz  26668  usgreqdrusgr  29496  pjini  31628  fzspl  32712  f1ocnt  32725  xrge0tsmsbi  33003  bnj983  34941  poimirlem16  37630  poimirlem19  37633  poimirlem25  37639  ac6s6  38166  fouriersw  46229  etransclem25  46257  ismea  46449  bits0oALTV  47679  uzlidlring  48220  linccl  48400  resinsnlem  48856  isinito2  49485  termc2  49504  discsntermlem  49556