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  5400  relsnb  5815  ffdm  6766  ov  7577  ovg  7598  oacl  8572  nnacl  8648  elpm2r  8884  djuxpdom  10224  djufi  10225  cfcof  10312  hargch  10711  uzaddcl  12944  expcllem  14110  lcmfval  16655  lcmf0val  16656  mreunirn  17646  filunirn  23906  ustelimasn  24247  metustfbas  24586  zrtelqelz  26816  usgreqdrusgr  29601  pjini  31728  fzspl  32798  f1ocnt  32810  xrge0tsmsbi  33049  bnj983  34944  poimirlem16  37623  poimirlem19  37626  poimirlem25  37632  ac6s6  38159  fouriersw  46187  etransclem25  46215  ismea  46407  bits0oALTV  47606  uzlidlring  48079  linccl  48260