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  1568  nfal  1599  19.9hd  1685  equsexd  1752  sbcof2  1833  aev  1835  sbequi  1862  nfsbd  2005  mo2n  2082  eupickb  2135  r19.29af2  2646  spc2gv  2864  spc3gv  2866  eqvincg  2897  sbcco3g  3151  ssrmof  3256  exmidsssnc  4248  exmid1stab  4253  snelpwi  4257  opth1  4281  frind  4400  onin  4434  abnexg  4494  reusv1  4506  xpexg  4790  dmexg  4943  rnexg  4944  elrelimasn  5049  relfld  5212  funimaexglem  5358  funimaexg  5359  fabexg  5465  fsnd  5567  elfvm  5611  nfvres  5612  funimass4  5631  elfvmptrab1  5676  funconstss  5700  f1oresrab  5747  resfunexg  5807  f1eqcocnv  5862  isores1  5885  isoini  5889  isose  5892  isopolem  5893  isosolem  5895  eusvobj2  5932  acexmidlemcase  5941  oprabid  5978  offval  6168  resfunexgALT  6195  offval3  6221  1stvalg  6230  2ndvalg  6231  1stcof  6251  2ndcof  6252  cnvf1o  6313  tposf12  6357  smores3  6381  smoiso  6390  tfr0dm  6410  tfrlemibxssdm  6415  tfrlemi14d  6421  tfrexlem  6422  tfr1onlemssrecs  6427  tfr1onlemsucfn  6428  tfr1onlemsucaccv  6429  tfr1onlembxssdm  6431  tfr1onlemres  6437  tfri1dALT  6439  tfrcllemssrecs  6440  tfrcllemsucfn  6441  tfrcllemsucaccv  6442  tfrcllembxssdm  6444  tfrcllemres  6450  rdgss  6471  nnsucsssuc  6580  nntr2  6591  swoord1  6651  swoord2  6652  iinerm  6696  eroveu  6715  pmresg  6765  en1uniel  6898  pw2f1odclem  6933  fopwdom  6935  xpen  6944  ssenen  6950  isinfinf  6996  ac6sfi  6997  preimaf1ofi  7055  sbthlem1  7061  fi0  7079  fiss  7081  supubti  7103  suplubti  7104  isotilem  7110  supisolem  7112  supisoex  7113  supisoti  7114  ordiso2  7139  eldju1st  7175  eldju2ndl  7176  updjud  7186  djudom  7197  ctmlemr  7212  enumctlemm  7218  nnnninfeq  7232  ctssexmid  7254  nninfwlpoimlemginf  7280  exmidonfinlem  7303  en2other2  7306  exmidaclem  7322  cc2lem  7380  cc3  7382  addclnq  7490  mulclnq  7491  1qec  7503  prarloclemarch2  7534  enq0tr  7549  addclnq0  7566  mulclnq0  7567  nq0m0r  7571  prarloclemlo  7609  prarloc  7618  genpml  7632  genpmu  7633  addnqprl  7644  addnqpru  7645  recnnpr  7663  prmuloc2  7682  1idpru  7706  ltexprlemm  7715  ltexprlemloc  7722  recexprlemm  7739  recexprlem1ssl  7748  caucvgprlemnkj  7781  caucvgprlemnbj  7782  caucvgprlemm  7783  caucvgprlemopl  7784  caucvgprlemlol  7785  caucvgprlemladdfu  7792  caucvgprlemladdrl  7793  caucvgprprlemk  7798  caucvgprprlemloccalc  7799  caucvgprprlemnkltj  7804  caucvgprprlemnjltk  7806  caucvgprprlemml  7809  caucvgprprlemmu  7810  caucvgprprlemlol  7813  caucvgprprlemexb  7822  caucvgprprlem1  7824  suplocexprlemml  7831  suplocexprlemlub  7839  addclsr  7868  mulclsr  7869  prsrcl  7899  caucvgsrlemoffcau  7913  peano5nnnn  8007  mulap0r  8690  nn1suc  9057  prime  9474  zindd  9493  xrlttri3  9921  xnn0xadd0  9991  fzopth  10185  fzsuc  10193  fzpred  10194  fzp1ss  10197  fztp  10202  fseq1p1m1  10218  1fv  10263  elfzom1elp1fzo  10333  ssfzo12  10355  fzosplitsn  10364  zsupcllemstep  10374  zsupcllemex  10375  infssuzledc  10379  divfl0  10441  fldiv4lem1div2uz2  10451  modqid  10496  modqmuladdim  10514  frecuzrdgtcl  10559  frecuzrdgfunlem  10566  frecfzennn  10573  frecfzen2  10574  seq3val  10607  seqvalcd  10608  seqsplitg  10636  iseqf1olemqcl  10646  iseqf1olemnab  10648  iseqf1olemmo  10652  iseqf1olemqk  10654  seq3f1olemstep  10661  seqf1oglem2  10667  seq3id3  10671  seqhomog  10677  faclbnd  10888  faclbnd3  10890  bcm1k  10907  hashfz1  10930  hashfz  10968  hashfzp1  10971  fiubm  10975  hashfacen  10983  leisorel  10984  wrdexb  11008  wrdsymb  11023  wrdred1hash  11039  lsw0  11043  lswex  11047  ccat0  11055  ccatval2  11057  ccats1val2  11095  swrds1  11124  swrdlsw  11125  cjcj  11227  caucvgre  11325  r19.2uz  11337  resqrexlemgt0  11364  ltabs  11431  xrmaxiflemab  11591  xrmaxiflemlub  11592  nnf1o  11720  summodclem2a  11725  fsumf1o  11734  fisum0diag2  11791  modfsummodlemstep  11801  fsumparts  11814  clim2prod  11883  prodfap0  11889  prodmodclem2a  11920  fprodssdc  11934  fprodcllem  11950  ef0lem  12004  resinval  12059  recosval  12060  demoivreALT  12118  nn0o  12251  gcdmultiplez  12375  dvdssq  12385  nninfct  12395  eucalg  12414  lcmgcdnn  12437  dvdsnprmd  12480  prm2orodd  12481  isprm5lem  12496  qnumdenbi  12547  nn0gcdsq  12555  phibnd  12572  hashdvds  12576  phimullem  12580  prmdiveq  12591  hashgcdlem  12593  modprm0  12610  nnnn0modprm0  12611  modprmn0modprm0  12612  oddprm  12615  prm23lt5  12619  pcprendvds  12646  pcidlem  12679  pcmpt  12699  pcfac  12706  infpnlem2  12716  prmunb  12718  1arith  12723  4sqlem19  12765  unennn  12801  ennnfonelemk  12804  ennnfonelemjn  12806  ennnfonelemhf1o  12817  ennnfonelemex  12818  ennnfonelemf1  12822  ennnfonelemrn  12823  qnnen  12835  unbendc  12858  setsfun0  12901  srngbased  13012  srngplusgd  13013  srngmulrd  13014  srnginvld  13015  lmodbased  13030  lmodplusgd  13031  lmodscad  13032  lmodvscad  13033  ipsbased  13042  ipsaddgd  13043  ipsmulrd  13044  ipsscad  13045  ipsvscad  13046  ipsipd  13047  tgval  13127  prdsbas3  13152  isnsgrp  13271  ismnd  13284  dfgrp2e  13393  subgintm  13567  eqg0el  13598  ecqusaddcl  13608  kerf1ghm  13643  gsumfzconst  13710  imasrng  13751  srgisid  13781  srg1zr  13782  qusring2  13861  oppr1g  13877  dvdsr02  13900  isunitd  13901  crngunit  13906  unitpropdg  13943  elrhmunit  13972  subrngintm  14007  subrguss  14031  subrgunit  14034  subrgugrp  14035  subrgintm  14038  lmodfopnelem1  14119  rmodislmodlem  14145  rmodislmod  14146  lssuni  14158  islss3  14174  lss0v  14225  sraval  14232  rnglidlmmgm  14291  2idllidld  14301  2idlridld  14302  rng2idl0  14314  rng2idlsubg0  14317  zrh0  14420  znle  14432  zndvds0  14445  znf1o  14446  znleval  14448  znfi  14450  znhash  14451  znunit  14454  psrbasg  14469  psradd  14474  psr0cl  14476  mpladd  14499  cldval  14604  ntrfval  14605  clsfval  14606  neifval  14645  neif  14646  neival  14648  cnclima  14728  cncnpi  14733  cnrest2  14741  cnrest2r  14742  cnptoprest  14744  cnpdis  14747  txvalex  14759  txval  14760  txcnmpt  14778  txdis  14782  cnmpt1t  14790  cnmpt2t  14798  hmeocnv  14812  hmeontr  14818  txhmeo  14824  xmetunirn  14863  xmettpos  14875  metn0  14883  xmetres  14887  metres  14888  blrnps  14916  blrn  14917  blin2  14937  blbas  14938  xmeterval  14940  xmettxlem  15014  xmettx  15015  metcnpi  15020  reldvg  15184  dvaddxx  15208  dvmulxx  15209  dviaddf  15210  dvimulf  15211  dvfre  15215  dvmptid  15221  dveflem  15231  elply2  15240  plyreres  15269  sinq12gt0  15335  rprelogbdiv  15462  logbgcd1irr  15472  fsumdvdsmul  15496  lgslem4  15513  lgsdirprm  15544  gausslemma2dlem0a  15559  gausslemma2dlem0f  15564  gausslemma2dlem0i  15567  gausslemma2dlem1a  15568  gausslemma2dlem1cl  15569  gausslemma2dlem5  15576  gausslemma2dlem6  15577  gausslemma2d  15579  lgseisenlem1  15580  lgseisenlem2  15581  lgseisenlem3  15582  lgseisen  15584  lgsquadlem1  15587  m1lgs  15595  2lgslem1a  15598  2lgslem1c  15600  2lgsoddprmlem2  15616  edgstruct  15691  bj-inex  15880  bj-sucexg  15895  bj-peano4  15928  setindis  15940  bdsetindis  15942  bj-inf2vnlem1  15943  nnsf  15979  nninfall  15983  nninfsellemeq  15988  sbthom  16002