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  1862  ax16i  1907  nelneq  2335  nelneq2  2336  nelne1  2504  nelne2  2505  spc2gv  2910  spc3gv  2912  nssne1  3300  nssne2  3301  ifbothdc  3661  ifpprsnssdc  3804  difsn  3836  iununir  4080  nbrne1  4133  nbrne2  4134  ss1o0el1  4315  mosubopt  4820  issref  5150  ssimaex  5743  chfnrn  5794  ffnfv  5840  f1elima  5952  dftpos4  6507  tfr1onlemsucaccv  6585  tfrcllemsucaccv  6598  snon0  7215  en2prde  7503  exmidonfinlem  7509  enq0sym  7763  prop  7806  prubl  7817  negf1o  8672  0fz1  10399  elfzmlbp  10488  swrdnd  11376  maxleast  11923  negfi  11938  isprm2  12839  nprmdvds1  12862  oddprmdvds  13077  ushgredgedg  16347  ushgredgedgloop  16349  loopclwwlkn1b  16540  clwwlkext2edg  16543  eupth2lem3lem4fi  16594  exmidsbthrlem  16928