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  5327  relsnb  5737  ffdm  6675  ov  7485  ovg  7506  oacl  8445  nnacl  8521  elpm2r  8764  djuxpdom  10072  djufi  10073  cfcof  10160  hargch  10559  uzaddcl  12797  expcllem  13974  lcmfval  16527  lcmf0val  16528  mreunirn  17498  filunirn  23792  ustelimasn  24133  metustfbas  24467  zrtelqelz  26690  usgreqdrusgr  29542  pjini  31671  fzspl  32764  f1ocnt  32774  xrge0tsmsbi  33035  bnj983  34955  poimirlem16  37676  poimirlem19  37679  poimirlem25  37685  ac6s6  38212  fouriersw  46269  etransclem25  46297  ismea  46489  bits0oALTV  47712  uzlidlring  48266  linccl  48446  resinsnlem  48902  isinito2  49531  termc2  49550  discsntermlem  49602