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  1483  ax16  1861  ax16i  1906  nelneq  2332  nelneq2  2333  nelne1  2492  nelne2  2493  spc2gv  2897  spc3gv  2899  nssne1  3285  nssne2  3286  ifbothdc  3640  ifpprsnssdc  3779  difsn  3810  iununir  4054  nbrne1  4107  nbrne2  4108  ss1o0el1  4287  mosubopt  4791  issref  5119  ssimaex  5707  chfnrn  5758  ffnfv  5805  f1elima  5913  dftpos4  6428  tfr1onlemsucaccv  6506  tfrcllemsucaccv  6519  snon0  7133  en2prde  7397  exmidonfinlem  7403  enq0sym  7651  prop  7694  prubl  7705  negf1o  8560  0fz1  10279  elfzmlbp  10366  swrdnd  11239  maxleast  11773  negfi  11788  isprm2  12688  nprmdvds1  12711  oddprmdvds  12926  ushgredgedg  16076  ushgredgedgloop  16078  loopclwwlkn1b  16269  clwwlkext2edg  16272  exmidsbthrlem  16626