Theorem ibir 267

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

Syntax hints:   → wi 4   ↔ wb 205

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 206

This theorem is referenced by:  elimh  1083  eusv2i  5354  relsnb  5763  ffdm  6703  ov  7504  ovg  7524  oacl  8486  nnacl  8563  elpm2r  8790  djuxpdom  10130  djufi  10131  cfcof  10219  hargch  10618  uzaddcl  12838  expcllem  13988  lcmfval  16508  lcmf0val  16509  mreunirn  17495  filunirn  23270  ustelimasn  23611  metustfbas  23950  usgreqdrusgr  28579  pjini  30704  fzspl  31761  f1ocnt  31773  xrge0tsmsbi  31970  bnj983  33652  poimirlem16  36167  poimirlem19  36170  poimirlem25  36176  ac6s6  36704  zrtelqelz  40889  fouriersw  44592  etransclem25  44620  ismea  44812  bits0oALTV  45993  uzlidlring  46347  linccl  46615