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 ) )

This proof depends on syntax axioms:   -> wi 4   <-> wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106

This proof depends on definitions:  df-bi 117

This theorem is used by:  biimpac  298  3impexpbicom  1488  ax16  1866  ax16i  1911  nelneq  2339  nelneq2  2340  nelne1  2510  nelne2  2511  spc2gv  2916  spc3gv  2918  nssne1  3306  nssne2  3307  ifbothdc  3675  ifpprsnssdc  3820  difsn  3852  iununir  4096  nbrne1  4150  nbrne2  4151  ss1o0el1  4336  mosubopt  4842  issref  5173  ssimaex  5767  chfnrn  5823  ffnfv  5869  f1elima  5982  dftpos4  6539  tfr1onlemsucaccv  6617  tfrcllemsucaccv  6630  snon0  7255  en2prde  7545  exmidonfinlem  7551  enq0sym  7805  prop  7848  prubl  7859  negf1o  8716  0fz1  10465  elfzmlbp  10555  swrdnd  11452  maxleast  12001  negfi  12016  isprm2  12919  nprmdvds1  12943  oddprmdvds  13161  assamulgscmlem2  15150  ushgredgedg  16689  ushgredgedgloop  16691  loopclwwlkn1b  16882  clwwlkext2edg  16885  eupth2lem3lem4fi  16936  exmidsbthrlem  17290