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 ⊢ (𝜑 → 𝜓)

This proof depends on syntax axioms:   → wi 4   ↔ wb 209

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210

This theorem is used by:  elimh  1099  eusv2i  5363  relsnb  5787  ffdm  6736  ov  7561  ovg  7582  oacl  8526  nnacl  8603  elpm2r  8848  djuxpdom  10192  djufi  10193  cfcof  10280  hargch  10686  uzaddcl  12957  expcllem  14140  lcmfval  16717  lcmf0val  16718  mreunirn  17691  filunirn  24114  ustelimasn  24455  metustfbas  24789  zrtelqelz  27003  usgreqdrusgr  30036  pjini  32188  fzspl  33268  f1ocnt  33279  xrge0tsmsbi  33522  bnj983  35468  kardenir  35692  kardnnfi  35703  poimirlem16  38393  poimirlem19  38396  poimirlem25  38402  ac6s6  38928  fouriersw  47067  etransclem25  47095  ismea  47287  bits0oALTV  48605  uzlidlring  49158  linccl  49352  resinsnlem  49805  isinito2  50433  termc2  50452  discsntermlem  50504