Theorem 3syl 17

Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
3syl	|- ( ph -> th )

Proof of Theorem 3syl

Step	Hyp	Ref	Expression
1		3syl.1	. . 3 |- ( ph -> ps )
2		3syl.2	. . 3 |- ( ps -> ch )
3	1, 2	syl 14	. 2 |- ( ph -> ch )
4		3syl.3	. 2 |- ( ch -> th )
5	3, 4	syl 14	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:  4syl  18  simpl2im  386  hbim  1545  nfal  1576  19.9hd  1662  equsexd  1729  sbcof2  1810  aev  1812  sbequi  1839  nfsbd  1977  mo2n  2054  eupickb  2107  r19.29af2  2617  spc2gv  2830  spc3gv  2832  eqvincg  2863  sbcco3g  3116  ssrmof  3220  exmidsssnc  4205  exmid1stab  4210  snelpwi  4214  opth1  4238  frind  4354  onin  4388  abnexg  4448  reusv1  4460  xpexg  4742  dmexg  4893  rnexg  4894  elrelimasn  4996  relfld  5159  funimaexglem  5301  funimaexg  5302  fabexg  5405  fsnd  5506  nfvres  5550  funimass4  5568  elfvmptrab1  5612  funconstss  5636  f1oresrab  5683  resfunexg  5739  f1eqcocnv  5794  isores1  5817  isoini  5821  isose  5824  isopolem  5825  isosolem  5827  eusvobj2  5863  acexmidlemcase  5872  oprabid  5909  offval  6092  resfunexgALT  6111  offval3  6137  1stvalg  6145  2ndvalg  6146  1stcof  6166  2ndcof  6167  cnvf1o  6228  tposf12  6272  smores3  6296  smoiso  6305  tfr0dm  6325  tfrlemibxssdm  6330  tfrlemi14d  6336  tfrexlem  6337  tfr1onlemssrecs  6342  tfr1onlemsucfn  6343  tfr1onlemsucaccv  6344  tfr1onlembxssdm  6346  tfr1onlemres  6352  tfri1dALT  6354  tfrcllemssrecs  6355  tfrcllemsucfn  6356  tfrcllemsucaccv  6357  tfrcllembxssdm  6359  tfrcllemres  6365  rdgss  6386  nnsucsssuc  6495  nntr2  6506  swoord1  6566  swoord2  6567  iinerm  6609  eroveu  6628  pmresg  6678  en1uniel  6806  fopwdom  6838  xpen  6847  ssenen  6853  isinfinf  6899  ac6sfi  6900  preimaf1ofi  6952  sbthlem1  6958  fi0  6976  fiss  6978  supubti  7000  suplubti  7001  isotilem  7007  supisolem  7009  supisoex  7010  supisoti  7011  ordiso2  7036  eldju1st  7072  eldju2ndl  7073  updjud  7083  djudom  7094  ctmlemr  7109  enumctlemm  7115  nnnninfeq  7128  ctssexmid  7150  nninfwlpoimlemginf  7176  exmidonfinlem  7194  en2other2  7197  exmidaclem  7209  cc2lem  7267  cc3  7269  addclnq  7376  mulclnq  7377  1qec  7389  prarloclemarch2  7420  enq0tr  7435  addclnq0  7452  mulclnq0  7453  nq0m0r  7457  prarloclemlo  7495  prarloc  7504  genpml  7518  genpmu  7519  addnqprl  7530  addnqpru  7531  recnnpr  7549  prmuloc2  7568  1idpru  7592  ltexprlemm  7601  ltexprlemloc  7608  recexprlemm  7625  recexprlem1ssl  7634  caucvgprlemnkj  7667  caucvgprlemnbj  7668  caucvgprlemm  7669  caucvgprlemopl  7670  caucvgprlemlol  7671  caucvgprlemladdfu  7678  caucvgprlemladdrl  7679  caucvgprprlemk  7684  caucvgprprlemloccalc  7685  caucvgprprlemnkltj  7690  caucvgprprlemnjltk  7692  caucvgprprlemml  7695  caucvgprprlemmu  7696  caucvgprprlemlol  7699  caucvgprprlemexb  7708  caucvgprprlem1  7710  suplocexprlemml  7717  suplocexprlemlub  7725  addclsr  7754  mulclsr  7755  prsrcl  7785  caucvgsrlemoffcau  7799  peano5nnnn  7893  mulap0r  8574  nn1suc  8940  prime  9354  zindd  9373  xrlttri3  9799  xnn0xadd0  9869  fzopth  10063  fzsuc  10071  fzpred  10072  fzp1ss  10075  fztp  10080  fseq1p1m1  10096  1fv  10141  elfzom1elp1fzo  10204  ssfzo12  10226  fzosplitsn  10235  divfl0  10298  modqid  10351  modqmuladdim  10369  frecuzrdgtcl  10414  frecuzrdgfunlem  10421  frecfzennn  10428  frecfzen2  10429  seq3val  10460  seqvalcd  10461  iseqf1olemqcl  10488  iseqf1olemnab  10490  iseqf1olemmo  10494  iseqf1olemqk  10496  seq3f1olemstep  10503  seq3id3  10509  faclbnd  10723  faclbnd3  10725  bcm1k  10742  hashfz1  10765  hashfz  10803  hashfzp1  10806  fiubm  10810  hashfacen  10818  leisorel  10819  cjcj  10894  caucvgre  10992  r19.2uz  11004  resqrexlemgt0  11031  ltabs  11098  xrmaxiflemab  11257  xrmaxiflemlub  11258  nnf1o  11386  summodclem2a  11391  fsumf1o  11400  fisum0diag2  11457  modfsummodlemstep  11467  fsumparts  11480  clim2prod  11549  prodfap0  11555  prodmodclem2a  11586  fprodssdc  11600  fprodcllem  11616  ef0lem  11670  resinval  11725  recosval  11726  demoivreALT  11783  nn0o  11914  zsupcllemstep  11948  zsupcllemex  11949  infssuzledc  11953  gcdmultiplez  12024  dvdssq  12034  eucalg  12061  lcmgcdnn  12084  dvdsnprmd  12127  prm2orodd  12128  isprm5lem  12143  qnumdenbi  12194  nn0gcdsq  12202  phibnd  12219  hashdvds  12223  phimullem  12227  prmdiveq  12238  hashgcdlem  12240  modprm0  12256  nnnn0modprm0  12257  modprmn0modprm0  12258  oddprm  12261  prm23lt5  12265  pcprendvds  12292  pcidlem  12324  pcmpt  12343  pcfac  12350  infpnlem2  12360  prmunb  12362  1arith  12367  unennn  12400  ennnfonelemk  12403  ennnfonelemjn  12405  ennnfonelemhf1o  12416  ennnfonelemex  12417  ennnfonelemf1  12421  ennnfonelemrn  12422  qnnen  12434  unbendc  12457  setsfun0  12500  srngbased  12607  srngplusgd  12608  srngmulrd  12609  srnginvld  12610  lmodbased  12625  lmodplusgd  12626  lmodscad  12627  lmodvscad  12628  ipsbased  12637  ipsaddgd  12638  ipsmulrd  12639  ipsscad  12640  ipsvscad  12641  ipsipd  12642  tgval  12716  isnsgrp  12817  ismnd  12825  dfgrp2e  12908  subgintm  13063  srgisid  13174  srg1zr  13175  oppr1g  13257  dvdsr02  13279  isunitd  13280  crngunit  13285  unitpropdg  13322  subrguss  13362  subrgunit  13365  subrgugrp  13366  subrgintm  13369  lmodfopnelem1  13419  rmodislmodlem  13445  rmodislmod  13446  lssuni  13455  islss3  13471  cldval  13638  ntrfval  13639  clsfval  13640  neifval  13679  neif  13680  neival  13682  cnclima  13762  cncnpi  13767  cnrest2  13775  cnrest2r  13776  cnptoprest  13778  cnpdis  13781  txvalex  13793  txval  13794  txcnmpt  13812  txdis  13816  cnmpt1t  13824  cnmpt2t  13832  hmeocnv  13846  hmeontr  13852  txhmeo  13858  xmetunirn  13897  xmettpos  13909  metn0  13917  xmetres  13921  metres  13922  blrnps  13950  blrn  13951  blin2  13971  blbas  13972  xmeterval  13974  xmettxlem  14048  xmettx  14049  metcnpi  14054  reldvg  14187  dvaddxx  14206  dvmulxx  14207  dviaddf  14208  dvimulf  14209  dvfre  14213  dveflem  14226  sinq12gt0  14290  rprelogbdiv  14414  logbgcd1irr  14424  lgslem4  14443  lgsdirprm  14474  lgseisenlem1  14489  lgseisenlem2  14490  m1lgs  14491  2lgsoddprmlem2  14493  bj-inex  14698  bj-sucexg  14713  bj-peano4  14746  setindis  14758  bdsetindis  14760  bj-inf2vnlem1  14761  nnsf  14793  nninfall  14797  nninfsellemeq  14802  sbthom  14813