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  5356  relsnb  5780  ffdm  6737  ov  7562  ovg  7583  oacl  8536  nnacl  8613  elpm2r  8858  djuxpdom  10257  djufi  10258  cfcof  10345  hargch  10751  uzaddcl  13024  expcllem  14208  lcmfval  16789  lcmf0val  16790  mreunirn  17764  filunirn  24194  ustelimasn  24535  metustfbas  24869  zrtelqelz  27079  usgreqdrusgr  30142  pjini  32294  fzspl  33374  f1ocnt  33385  xrge0tsmsbi  33628  bnj983  35574  kardenir  35809  kardnnfi  35820  poimirlem16  38534  poimirlem19  38537  poimirlem25  38543  ac6s6  39084  fouriersw  47210  etransclem25  47238  ismea  47430  bits0oALTV  48748  uzlidlring  49301  linccl  49495  resinsnlem  49948  isinito2  50576  termc2  50595  discsntermlem  50647