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  5394  relsnb  5812  ffdm  6765  ov  7577  ovg  7598  oacl  8573  nnacl  8649  elpm2r  8885  djuxpdom  10226  djufi  10227  cfcof  10314  hargch  10713  uzaddcl  12946  expcllem  14113  lcmfval  16658  lcmf0val  16659  mreunirn  17644  filunirn  23890  ustelimasn  24231  metustfbas  24570  zrtelqelz  26801  usgreqdrusgr  29586  pjini  31718  fzspl  32791  f1ocnt  32804  xrge0tsmsbi  33066  bnj983  34965  poimirlem16  37643  poimirlem19  37646  poimirlem25  37652  ac6s6  38179  fouriersw  46246  etransclem25  46274  ismea  46466  bits0oALTV  47668  uzlidlring  48151  linccl  48331  resinsnlem  48771  termc2  49148