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  5336  relsnb  5748  ffdm  6688  ov  7499  ovg  7520  oacl  8459  nnacl  8535  elpm2r  8778  djuxpdom  10088  djufi  10089  cfcof  10176  hargch  10575  uzaddcl  12808  expcllem  13986  lcmfval  16539  lcmf0val  16540  mreunirn  17511  filunirn  23817  ustelimasn  24158  metustfbas  24492  zrtelqelz  26715  usgreqdrusgr  29568  pjini  31700  fzspl  32797  f1ocnt  32808  xrge0tsmsbi  33084  bnj983  35035  poimirlem16  37749  poimirlem19  37752  poimirlem25  37758  ac6s6  38285  fouriersw  46391  etransclem25  46419  ismea  46611  bits0oALTV  47843  uzlidlring  48397  linccl  48576  resinsnlem  49032  isinito2  49660  termc2  49679  discsntermlem  49731