Theorem sylc 56

Description: A syllogism inference combined with contraction. (Contributed by NM, 4-May-1994.) (Revised by NM, 13-Jul-2013.)

Hypotheses

Ref	Expression
sylc.1	|- ( ph -> ps )
sylc.2	|- ( ph -> ch )
sylc.3	|- ( ps -> ( ch -> th ) )

Assertion

Ref	Expression
sylc	|- ( ph -> th )

Proof of Theorem sylc

Step	Hyp	Ref	Expression
1		sylc.1	. . 3 |- ( ph -> ps )
2		sylc.2	. . 3 |- ( ph -> ch )
3		sylc.3	. . 3 |- ( ps -> ( ch -> th ) )
4	1, 2, 3	syl2im 34	. 2 |- ( ph -> ( ph -> th ) )
5	4	pm2.43i 43	1 |- ( ph -> th )

Syntax hints:   -> wi 4

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7

This theorem is referenced by:  syl3c  57  mpsyl  59  imp  115  2thd  164  jca  290  syl2anc  391  jc  580  annimdc  845  dn1dc  867  xordidc  1290  nfimd  1477  exlimd2  1486  elex22  2569  elex2  2570  spcimdv  2637  spcimedv  2639  spsbcd  2776  opth  3974  euotd  3991  ssorduni  4213  wetriext  4301  tfisi  4310  sotri2  4722  sotri3  4723  unielrel  4845  funmo  4917  fnfvima  5393  fliftfun  5436  fliftval  5440  riota5f  5492  riotass2  5494  grprinvlem  5695  grprinvd  5696  caofref  5732  tfrlem1  5923  tfrlem5  5930  tfrlemibxssdm  5941  tfrlemibfn  5942  tfrlemiex  5945  rdgisucinc  5972  frecabex  5984  ertr  6121  qliftlem  6184  th3q  6211  f1dom2g  6236  dom3d  6254  en1  6279  xpdom3m  6308  phplem4dom  6324  phpm  6327  phpelm  6328  findcard  6345  ordiso2  6357  recexnq  6488  ltbtwnnqq  6513  addnnnq0  6547  mulnnnq0  6548  prltlu  6585  prarloclemn  6597  prarloc  6601  distrlem1prl  6680  distrlem1pru  6681  distrlem4prl  6682  distrlem4pru  6683  ltexprlemrl  6708  cauappcvgprlemladdru  6754  cauappcvgprlemladdrl  6755  caucvgprprlemml  6792  addsrpr  6830  mulsrpr  6831  axcaucvglemres  6973  lemul12a  7828  lemulge11  7832  nngt0  7939  nn0ge0  8207  nn0ge2m1nn  8242  zletric  8289  zlelttric  8290  nn0n0n1ge2b  8320  nn0ind-raph  8355  rpge0  8595  fz0fzelfz0  8984  fz0fzdiffz0  8987  ige2m2fzo  9054  elfzodifsumelfzo  9057  elfzom1elp1fzo  9058  qletric  9099  qlelttric  9100  qbtwnzlemshrink  9104  rebtwn2zlemshrink  9108  frecuzrdgfn  9198  frecuzrdg0  9200  frecfzennn  9203  iseqovex  9219  iseqfn  9221  iseq1  9222  iseqcl  9223  iseqp1  9225  iseqfveq2  9228  iseqfveq  9230  iseqshft2  9232  monoord  9235  monoord2  9236  isermono  9237  iseqsplit  9238  iseqcaopr3  9240  iseqid3s  9246  iseqid  9247  iseqhomo  9248  expcl2lemap  9267  leexp1a  9309  expnbnd  9372  cvg1nlemcau  9583  cvg1nlemres  9584  recvguniq  9593  resqrexlemdecn  9610  resqrexlemgt0  9618  resqrexlemoverl  9619  resqrexlemglsq  9620  cau3lem  9710  climi  9808  climcn1  9829  climcn2  9830  ialgfx  9891