Theorem ibir 270

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 225	. 2 ⊢ (𝜑 → (𝜑 ↔ 𝜓))
3	2	ibi 269	1 ⊢ (𝜑 → 𝜓)

Syntax hints:   → wi 4   ↔ wb 208

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 209

This theorem is referenced by:  elimh  1093  eusv2i  5348  relsnb  5771  ffdm  6716  ov  7535  ovg  7556  oacl  8498  nnacl  8575  elpm2r  8820  djuxpdom  10136  djufi  10137  cfcof  10225  hargch  10625  uzaddcl  12899  expcllem  14079  lcmfval  16646  lcmf0val  16647  mreunirn  17620  filunirn  23930  ustelimasn  24271  metustfbas  24605  zrtelqelz  26811  usgreqdrusgr  29726  pjini  31859  fzspl  32952  f1ocnt  32963  xrge0tsmsbi  33215  bnj983  35207  poimirlem16  38096  poimirlem19  38099  poimirlem25  38105  ac6s6  38632  fouriersw  46766  etransclem25  46794  ismea  46986  bits0oALTV  48264  uzlidlring  48818  linccl  48997  resinsnlem  49453  isinito2  50081  termc2  50100  discsntermlem  50152