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  1081  eusv2i  5312  relsnb  5701  ffdm  6614  ov  7395  ovg  7415  oacl  8327  nnacl  8404  elpm2r  8591  djuxpdom  9872  djufi  9873  cfcof  9961  hargch  10360  uzaddcl  12573  expcllem  13721  lcmfval  16254  lcmf0val  16255  mreunirn  17227  filunirn  22941  ustelimasn  23282  metustfbas  23619  usgreqdrusgr  27838  pjini  29962  fzspl  31013  f1ocnt  31025  xrge0tsmsbi  31220  bnj983  32831  poimirlem16  35720  poimirlem19  35723  poimirlem25  35729  ac6s6  36257  zrtelqelz  40266  fouriersw  43662  etransclem25  43690  ismea  43879  bits0oALTV  45021  uzlidlring  45375  linccl  45643