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  5412  relsnb  5826  ffdm  6777  ov  7594  ovg  7615  oacl  8591  nnacl  8667  elpm2r  8903  djuxpdom  10255  djufi  10256  cfcof  10343  hargch  10742  uzaddcl  12969  expcllem  14123  lcmfval  16668  lcmf0val  16669  mreunirn  17659  filunirn  23911  ustelimasn  24252  metustfbas  24591  zrtelqelz  26819  usgreqdrusgr  29604  pjini  31731  fzspl  32795  f1ocnt  32807  xrge0tsmsbi  33042  bnj983  34927  poimirlem16  37596  poimirlem19  37599  poimirlem25  37605  ac6s6  38132  fouriersw  46152  etransclem25  46180  ismea  46372  bits0oALTV  47555  uzlidlring  47958  linccl  48143