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  5749  ffdm  6685  ov  7497  ovg  7518  oacl  8460  nnacl  8536  elpm2r  8779  djuxpdom  10099  djufi  10100  cfcof  10187  hargch  10586  uzaddcl  12824  expcllem  13998  lcmfval  16551  lcmf0val  16552  mreunirn  17522  filunirn  23786  ustelimasn  24127  metustfbas  24462  zrtelqelz  26685  usgreqdrusgr  29533  pjini  31662  fzspl  32751  f1ocnt  32764  xrge0tsmsbi  33035  bnj983  34937  poimirlem16  37635  poimirlem19  37638  poimirlem25  37644  ac6s6  38171  fouriersw  46232  etransclem25  46260  ismea  46452  bits0oALTV  47685  uzlidlring  48239  linccl  48419  resinsnlem  48875  isinito2  49504  termc2  49523  discsntermlem  49575