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  1481  ax16  1859  ax16i  1904  nelneq  2330  nelneq2  2331  nelne1  2490  nelne2  2491  spc2gv  2894  spc3gv  2896  nssne1  3282  nssne2  3283  ifbothdc  3637  ifpprsnssdc  3774  difsn  3805  iununir  4049  nbrne1  4102  nbrne2  4103  ss1o0el1  4282  mosubopt  4786  issref  5114  ssimaex  5700  chfnrn  5751  ffnfv  5798  f1elima  5906  dftpos4  6420  tfr1onlemsucaccv  6498  tfrcllemsucaccv  6511  snon0  7118  en2prde  7382  exmidonfinlem  7387  enq0sym  7635  prop  7678  prubl  7689  negf1o  8544  0fz1  10258  elfzmlbp  10345  swrdnd  11212  maxleast  11745  negfi  11760  isprm2  12660  nprmdvds1  12683  oddprmdvds  12898  ushgredgedg  16045  ushgredgedgloop  16047  loopclwwlkn1b  16187  clwwlkext2edg  16190  exmidsbthrlem  16504