Theorem ibir 260

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

Syntax hints:   → wi 4   ↔ wb 198

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 199

This theorem is referenced by:  elimh  1061  eusv2i  5148  relsnb  5525  ffdm  6365  ov  7110  ovg  7129  oacl  7962  nnacl  8038  elpm2r  8224  djuxpdom  9409  djufi  9410  cfcof  9494  hargch  9893  uzaddcl  12118  expcllem  13255  lcmfval  15821  lcmf0val  15822  mreunirn  16730  filunirn  22194  ustelimasn  22534  metustfbas  22870  usgreqdrusgr  27053  pjini  29257  fzspl  30270  f1ocnt  30279  xrge0tsmsbi  30537  bnj983  31876  poimirlem16  34355  poimirlem19  34358  poimirlem25  34364  ac6s6  34900  zrtelqelz  38630  fouriersw  41953  etransclem25  41981  ismea  42170  bits0oALTV  43220  uzlidlring  43570  linccl  43842