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  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  5914  dftpos4  6429  tfr1onlemsucaccv  6507  tfrcllemsucaccv  6520  snon0  7134  en2prde  7398  exmidonfinlem  7404  enq0sym  7652  prop  7695  prubl  7706  negf1o  8561  0fz1  10280  elfzmlbp  10367  swrdnd  11244  maxleast  11791  negfi  11806  isprm2  12707  nprmdvds1  12730  oddprmdvds  12945  ushgredgedg  16096  ushgredgedgloop  16098  loopclwwlkn1b  16289  clwwlkext2edg  16292  eupth2lem3lem4fi  16343  exmidsbthrlem  16677