Theorem biimpcd 159

Description: Deduce a commuted implication from a logical equivalence. (Contributed by NM, 3-May-1994.) (Proof shortened by Wolf Lammen, 22-Sep-2013.)

Hypothesis

Ref	Expression
biimpcd.1	⊢ (𝜑 → (𝜓 ↔ 𝜒))

Assertion

Ref	Expression
biimpcd	⊢ (𝜓 → (𝜑 → 𝜒))

Proof of Theorem biimpcd

Step	Hyp	Ref	Expression
1		id 19	. 2 ⊢ (𝜓 → 𝜓)
2		biimpcd.1	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3	1, 2	syl5ibcom 155	1 ⊢ (𝜓 → (𝜑 → 𝜒))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  biimpac  298  3impexpbicom  1438  ax16  1813  ax16i  1858  nelneq  2278  nelneq2  2279  nelne1  2437  nelne2  2438  spc2gv  2829  spc3gv  2831  nssne1  3214  nssne2  3215  ifbothdc  3568  difsn  3730  iununir  3971  nbrne1  4023  nbrne2  4024  ss1o0el1  4198  mosubopt  4692  issref  5012  ssimaex  5578  chfnrn  5628  ffnfv  5675  f1elima  5774  dftpos4  6264  tfr1onlemsucaccv  6342  tfrcllemsucaccv  6355  snon0  6935  exmidonfinlem  7192  enq0sym  7431  prop  7474  prubl  7485  negf1o  8339  0fz1  10045  elfzmlbp  10132  maxleast  11222  negfi  11236  isprm2  12117  nprmdvds1  12140  oddprmdvds  12352  exmidsbthrlem  14773