Theorem sylc 62

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 38	. 2 |- ( ph -> ( ph -> th ) )
5	4	pm2.43i 49	1 |- ( ph -> th )

Syntax hints:   -> wi 4

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

This theorem is referenced by:  syl3c  63  mpsyl  65  imp  124  2thd  175  jca  306  syl2anc  411  jc  656  jcnd  658  annimdc  946  pm4.55dc  947  orandc  948  dn1dc  969  syl2an23an  1336  xordidc  1444  nfimd  1634  exlimd2  1644  elex22  2831  elex2  2832  spcimdv  2903  spcimedv  2905  spcedv  2908  rspcdva  2928  elabd  2964  spsbcd  3057  opth  4355  euotd  4373  ssorduni  4611  tfisi  4711  omsinds  4746  nnpredcl  4747  sotri2  5162  sotri3  5163  unielrel  5292  funmo  5369  fnfvima  5923  resfvresima  5925  fliftfun  5971  fliftval  5975  riota5f  6032  riotass2  6034  fovcld  6160  oprssdmm  6367  funsssuppss  6460  tfrlem5  6547  tfrlemibxssdm  6560  tfrlemibfn  6561  tfrlemiex  6564  tfr1onlemsucfn  6573  tfr1onlemsucaccv  6574  tfr1onlembxssdm  6576  tfr1onlembfn  6577  tfr1onlemex  6580  tfr1onlemres  6582  tfrcllemsucfn  6586  tfrcllemsucaccv  6587  tfrcllembxssdm  6589  tfrcllembfn  6590  tfrcllemex  6593  tfrcllemres  6595  tfrcl  6597  rdgisucinc  6618  frecabex  6631  frecabcl  6632  nntr2  6738  ertr  6784  qliftlem  6849  th3q  6876  resixp  6970  f1dom2g  6997  dom3d  7015  domssr  7019  en1  7041  xpdom3m  7087  xpf1o  7099  phplem4dom  7118  phpm  7122  phpelm  7123  findcard  7147  finexdc  7162  fiintim  7193  fisseneq  7197  ssfirab  7199  opabfi  7202  f1dmvrnfibi  7213  iunfidisj  7215  fidcenumlemrk  7226  dcfi  7270  2omapfi  7273  suplub2ti  7294  supelti  7295  ordiso2  7328  caseinl  7384  caseinr  7385  djudom  7386  difinfsn  7393  difinfinf  7394  ctm  7402  enumct  7408  nnnninfeq  7421  ismkvnex  7448  exmidfodomrlemr  7507  exmidfodomrlemrALT  7508  acfun  7516  exmidontriimlem2  7531  exmidontriimlem3  7532  exmidapne  7576  cc2lem  7582  cc3  7584  recexnq  7707  ltbtwnnqq  7732  addnnnq0  7766  mulnnnq0  7767  prarloclemn  7816  prarloc  7820  distrlem1prl  7899  distrlem1pru  7900  distrlem4prl  7901  distrlem4pru  7902  ltexprlemrl  7927  cauappcvgprlemladdru  7973  cauappcvgprlemladdrl  7974  addsrpr  8062  mulsrpr  8063  map2psrprg  8122  axpre-suploclemres  8218  lemul12a  9138  lemulge11  9142  sup3exmid  9233  nngt0  9264  nn0ge0  9523  nn0ge2m1nn  9562  zletric  9623  zlelttric  9624  nn0n0n1ge2b  9660  nn0ind-raph  9698  supinfneg  9930  infsupneg  9931  infregelbex  9933  rpge0  10002  fz0fzelfz0  10465  fz0fzdiffz0  10468  ige2m2fzo  10547  elfzodifsumelfzo  10550  elfzom1elp1fzo  10551  exfzdc  10590  zsupcllemstep  10593  infssuzex  10597  qletric  10605  qlelttric  10606  rebtwn2zlemshrink  10617  frecuzrdgtcl  10778  frecuzrdg0  10779  frecuzrdgfunlem  10785  frecuzrdg0t  10788  frecuzrdgsuctlem  10789  frecfzennn  10792  seq3f1olemstep  10880  expcl2lemap  10917  leexp1a  10960  expnbnd  11029  faclbnd  11107  faclbnd6  11110  facavg  11112  fihasheqf1oi  11154  fihashf1rn  11155  fihashss  11185  fiubm  11199  seq3coll  11218  wrdsymb0  11261  wrdlenge2n0  11264  ccatsymb  11294  pfxnd  11385  pfxccat1  11398  swrdpfx  11403  pfxpfx  11404  wrd2ind  11419  pfxccatin12  11429  pfxccat3  11430  swrdccat  11431  pfxccatpfx1  11432  pfxccatpfx2  11433  swrdccatin1d  11439  pfxccatin12d  11441  resqrexlemdecn  11701  qabsor  11764  cau3lem  11803  xrmaxiflemab  11936  xrmaxadd  11950  climcn2  11998  sumeq2  12048  sumrbdclem  12067  summodclem3  12070  summodclem2a  12071  zsumdc  12074  fsumgcl  12076  fsum3  12077  isumss  12081  fsumadd  12096  fsum2dlemstep  12124  fisum0diag2  12137  fsummulc2  12138  modfsummodlemstep  12147  fsumabs  12155  fsumrelem  12161  fsumiun  12167  isumshft  12180  mertenslem2  12226  prodeq2  12247  prodrbdclem  12261  prodmodclem3  12265  prodmodclem2a  12266  zproddc  12269  fprodseq  12273  fprodmul  12281  fprodconst  12310  fprodap0  12311  fprod2dlemstep  12312  fprodrec  12319  fprodsplit1f  12324  fprodap0f  12326  fprodle  12330  sin02gt0  12454  efieq1re  12462  p1modz1  12484  dvdsleabs2  12536  4dvdseven  12607  bitsfzo  12645  bitsinv1lem  12651  gcdeq0  12677  rppwr  12728  uzwodc  12737  algfx  12753  eucalgcvga  12759  lcmmndc  12763  lcmeq0  12772  qredeq  12797  isprm3  12819  rpexp  12854  sqpweven  12876  2sqpwodd  12877  phicl2  12915  phibnd  12918  phiprmpw  12923  fermltl  12935  pythagtriplem4  12970  pythagtriplem6  12972  pythagtriplem7  12973  pythagtriplem12  12977  pythagtriplem13  12978  pythagtriplem14  12979  pythagtriplem16  12981  pcdvdsb  13022  pc2dvds  13032  difsqpwdvds  13040  pcmpt  13045  pcmptdvds  13047  fldivp1  13050  prmpwdvds  13057  infpnlem1  13061  1arith  13069  4sqlem11  13103  ballotfilemfp1  13152  ennnfonelemk  13168  ennnfonelemhom  13183  ennnfonelemrnh  13184  ennnfonelemf1  13186  ctinf  13198  ctiunctlemudc  13205  ctiunctlemf  13206  nninfdclemp1  13218  strslfvd  13271  strslfv2d  13272  strslssd  13276  imasival  13536  imasbas  13537  imasplusg  13538  imasaddfnlemg  13544  imasaddvallemg  13545  qusaddvallemg  13563  qusaddflemg  13564  qusaddval  13565  qusaddf  13566  qusmulval  13567  qusmulf  13568  lidrididd  13612  gsumfzval  13621  sgrpidmndm  13650  gsumfzz  13725  qusgrp2  13847  mulgnegnn  13866  eqgen  13961  rinvmod  14043  gsumfzconst  14075  qusrng  14119  srgdilem  14130  ringdilem  14173  qusring2  14227  lssintclm  14549  gsumfzfsumlemm  14752  mplsubgfilemm  14870  eltg3  14939  iuncld  14997  cnss2  15109  txcnp  15153  uptx  15156  xblm  15299  metss  15376  fsumcncntop  15449  rescncf  15463  dedekindeulemlu  15503  suplociccex  15507  dedekindicclemlu  15512  dedekindicc  15515  ivthdec  15526  limccnp2lem  15558  dvaddxx  15585  dvmulxx  15586  dvrecap  15595  reeff1olem  15653  perfectlem2  15885  lgsval  15894  lgsfvalg  15895  lgsfcl2  15896  lgscllem  15897  lgsval2lem  15900  lgsneg  15914  lgsdir2  15923  lgsdir  15925  lgsdi  15927  lgsne0  15928  lgsdirnn0  15937  lgsdinn0  15938  gausslemma2dlem0c  15941  m1lgs  15975  2lgslem1  15981  2lgs  15994  2lgsoddprm  16003  2sqlem6  16010  incistruhgr  16102  upgredg  16156  uhgr2edg  16218  usgriedgdomord  16237  wlkpropg  16336  wlkvtxeledgg  16356  wlk2f  16363  clwwlknonccat  16445  clwwlknonex2lem2  16450  eupth2lem3lem4fi  16485  eupth2lem3lem7fi  16486  sumdc2  16588  pwle2  16789  subctctexmid  16791  nninfsellemeq  16809  nnnninfex  16817  exmidsbthrlem  16819  cndcap  16861  gfsump1  16885