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  5341  relsnb  5759  ffdm  6699  ov  7512  ovg  7533  oacl  8472  nnacl  8549  elpm2r  8794  djuxpdom  10108  djufi  10109  cfcof  10196  hargch  10596  uzaddcl  12829  expcllem  14007  lcmfval  16560  lcmf0val  16561  mreunirn  17532  filunirn  23838  ustelimasn  24179  metustfbas  24513  zrtelqelz  26736  usgreqdrusgr  29654  pjini  31787  fzspl  32880  f1ocnt  32891  xrge0tsmsbi  33168  bnj983  35127  poimirlem16  37887  poimirlem19  37890  poimirlem25  37896  ac6s6  38423  fouriersw  46589  etransclem25  46617  ismea  46809  bits0oALTV  48041  uzlidlring  48595  linccl  48774  resinsnlem  49230  isinito2  49858  termc2  49877  discsntermlem  49929