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  5393  relsnb  5811  ffdm  6764  ov  7578  ovg  7599  oacl  8574  nnacl  8650  elpm2r  8886  djuxpdom  10227  djufi  10228  cfcof  10315  hargch  10714  uzaddcl  12947  expcllem  14114  lcmfval  16659  lcmf0val  16660  mreunirn  17645  filunirn  23891  ustelimasn  24232  metustfbas  24571  zrtelqelz  26802  usgreqdrusgr  29587  pjini  31719  fzspl  32792  f1ocnt  32805  xrge0tsmsbi  33067  bnj983  34966  poimirlem16  37644  poimirlem19  37647  poimirlem25  37653  ac6s6  38180  fouriersw  46251  etransclem25  46279  ismea  46471  bits0oALTV  47673  uzlidlring  48156  linccl  48336  resinsnlem  48777  termc2  49176  discsntermlem  49222