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  1079  eusv2i  5281  relsnb  5661  ffdm  6522  ov  7280  ovg  7299  oacl  8146  nnacl  8223  elpm2r  8410  djuxpdom  9597  djufi  9598  cfcof  9682  hargch  10081  uzaddcl  12291  expcllem  13430  lcmfval  15948  lcmf0val  15949  mreunirn  16855  filunirn  22473  ustelimasn  22814  metustfbas  23150  usgreqdrusgr  27336  pjini  29460  fzspl  30499  f1ocnt  30511  xrge0tsmsbi  30700  bnj983  32230  poimirlem16  34942  poimirlem19  34945  poimirlem25  34951  ac6s6  35482  zrtelqelz  39267  fouriersw  42606  etransclem25  42634  ismea  42823  bits0oALTV  43931  uzlidlring  44285  linccl  44554