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

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

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimpac  298  3impexpbicom  1488  ax16  1866  ax16i  1911  nelneq  2339  nelneq2  2340  nelne1  2510  nelne2  2511  spc2gv  2916  spc3gv  2918  nssne1  3306  nssne2  3307  ifbothdc  3675  ifpprsnssdc  3820  difsn  3852  iununir  4096  nbrne1  4149  nbrne2  4150  ss1o0el1  4334  mosubopt  4840  issref  5170  ssimaex  5764  chfnrn  5820  ffnfv  5866  f1elima  5979  dftpos4  6534  tfr1onlemsucaccv  6612  tfrcllemsucaccv  6625  snon0  7249  en2prde  7540  exmidonfinlem  7546  enq0sym  7800  prop  7843  prubl  7854  negf1o  8711  0fz1  10460  elfzmlbp  10550  swrdnd  11447  maxleast  11996  negfi  12011  isprm2  12914  nprmdvds1  12938  oddprmdvds  13156  assamulgscmlem2  15126  ushgredgedg  16633  ushgredgedgloop  16635  loopclwwlkn1b  16826  clwwlkext2edg  16829  eupth2lem3lem4fi  16880  exmidsbthrlem  17233