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  5336  relsnb  5758  ffdm  6697  ov  7511  ovg  7532  oacl  8470  nnacl  8547  elpm2r  8792  djuxpdom  10108  djufi  10109  cfcof  10196  hargch  10596  uzaddcl  12854  expcllem  14034  lcmfval  16590  lcmf0val  16591  mreunirn  17563  filunirn  23847  ustelimasn  24188  metustfbas  24522  zrtelqelz  26722  usgreqdrusgr  29637  pjini  31770  fzspl  32862  f1ocnt  32873  xrge0tsmsbi  33135  bnj983  35093  poimirlem16  37957  poimirlem19  37960  poimirlem25  37966  ac6s6  38493  fouriersw  46659  etransclem25  46687  ismea  46879  bits0oALTV  48157  uzlidlring  48711  linccl  48890  resinsnlem  49346  isinito2  49974  termc2  49993  discsntermlem  50045