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	|- ( ph -> ( ps <-> ch ) )

Assertion

Ref	Expression
biimpcd	|- ( ps -> ( ph -> ch ) )

Proof of Theorem biimpcd

Step	Hyp	Ref	Expression
1		id 19	. 2 |- ( ps -> ps )
2		biimpcd.1	. 2 |- ( ph -> ( ps <-> ch ) )
3	1, 2	syl5ibcom 155	1 |- ( ps -> ( ph -> ch ) )

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  7458  exmidonfinlem  7464  enq0sym  7712  prop  7755  prubl  7766  negf1o  8620  0fz1  10342  elfzmlbp  10429  swrdnd  11306  maxleast  11853  negfi  11868  isprm2  12769  nprmdvds1  12792  oddprmdvds  13007  ushgredgedg  16167  ushgredgedgloop  16169  loopclwwlkn1b  16360  clwwlkext2edg  16363  eupth2lem3lem4fi  16414  exmidsbthrlem  16750