Theorem ibir 271

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

Syntax hints:   → wi 4   ↔ wb 209

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 210

This theorem is referenced by:  elimh  1099  eusv2i  5365  relsnb  5789  ffdm  6735  ov  7554  ovg  7575  oacl  8516  nnacl  8593  elpm2r  8838  djuxpdom  10165  djufi  10166  cfcof  10253  hargch  10653  uzaddcl  12923  expcllem  14104  lcmfval  16674  lcmf0val  16675  mreunirn  17648  filunirn  24039  ustelimasn  24380  metustfbas  24714  zrtelqelz  26923  usgreqdrusgr  29918  pjini  32051  fzspl  33134  f1ocnt  33145  xrge0tsmsbi  33394  bnj983  35339  kardenir  35571  kardnnfi  35582  poimirlem16  38287  poimirlem19  38290  poimirlem25  38296  ac6s6  38821  fouriersw  46945  etransclem25  46973  ismea  47165  bits0oALTV  48446  uzlidlring  49000  linccl  49194  resinsnlem  49649  isinito2  50277  termc2  50296  discsntermlem  50348