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  1484  ax16  1861  ax16i  1906  nelneq  2332  nelneq2  2333  nelne1  2493  nelne2  2494  spc2gv  2898  spc3gv  2900  nssne1  3286  nssne2  3287  ifbothdc  3644  ifpprsnssdc  3783  difsn  3815  iununir  4059  nbrne1  4112  nbrne2  4113  ss1o0el1  4293  mosubopt  4797  issref  5126  ssimaex  5716  chfnrn  5767  ffnfv  5813  f1elima  5924  dftpos4  6472  tfr1onlemsucaccv  6550  tfrcllemsucaccv  6563  snon0  7177  en2prde  7441  exmidonfinlem  7447  enq0sym  7695  prop  7738  prubl  7749  negf1o  8603  0fz1  10325  elfzmlbp  10412  swrdnd  11289  maxleast  11836  negfi  11851  isprm2  12752  nprmdvds1  12775  oddprmdvds  12990  ushgredgedg  16150  ushgredgedgloop  16152  loopclwwlkn1b  16343  clwwlkext2edg  16346  eupth2lem3lem4fi  16397  exmidsbthrlem  16733