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  1591  nfal  1622  19.9hd  1708  equsexd  1775  sbcof2  1856  aev  1858  sbequi  1885  nfsbd  2028  mo2n  2105  eupickb  2159  r19.29af2  2671  spc2gv  2894  spc3gv  2896  eqvincg  2927  sbcco3g  3182  ssrmof  3287  exmidsssnc  4287  exmid1stab  4292  snelpwi  4297  opth1  4322  frind  4443  onin  4477  abnexg  4537  reusv1  4549  xpexg  4833  reldmm  4942  dmexg  4988  rnexg  4989  elrelimasn  5094  relfld  5257  funimaexglem  5404  funimaexg  5405  fabexg  5515  fsnd  5618  elfvm  5662  nfvres  5665  funimass4  5686  elfvmptrab1  5731  funconstss  5755  f1oresrab  5802  resfunexg  5864  f1eqcocnv  5921  isores1  5944  isoini  5948  isose  5951  isopolem  5952  isosolem  5954  eusvobj2  5993  acexmidlemcase  6002  oprabid  6039  offval  6232  resfunexgALT  6259  offval3  6285  1stvalg  6294  2ndvalg  6295  1stcof  6315  2ndcof  6316  cnvf1o  6377  tposf12  6421  smores3  6445  smoiso  6454  tfr0dm  6474  tfrlemibxssdm  6479  tfrlemi14d  6485  tfrexlem  6486  tfr1onlemssrecs  6491  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlemres  6501  tfri1dALT  6503  tfrcllemssrecs  6504  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemres  6514  rdgss  6535  nnsucsssuc  6646  nntr2  6657  swoord1  6717  swoord2  6718  iinerm  6762  eroveu  6781  pmresg  6831  en1uniel  6964  dom1o  6985  pw2f1odclem  7003  fopwdom  7005  xpen  7014  ssenen  7020  isinfinf  7067  ac6sfi  7068  preimaf1ofi  7129  sbthlem1  7135  fi0  7153  fiss  7155  supubti  7177  suplubti  7178  isotilem  7184  supisolem  7186  supisoex  7187  supisoti  7188  ordiso2  7213  eldju1st  7249  eldju2ndl  7250  updjud  7260  djudom  7271  ctmlemr  7286  enumctlemm  7292  nnnninfeq  7306  ctssexmid  7328  nninfwlpoimlemginf  7354  exmidonfinlem  7382  en2other2  7385  exmidaclem  7401  cc2lem  7463  cc3  7465  addclnq  7573  mulclnq  7574  1qec  7586  prarloclemarch2  7617  enq0tr  7632  addclnq0  7649  mulclnq0  7650  nq0m0r  7654  prarloclemlo  7692  prarloc  7701  genpml  7715  genpmu  7716  addnqprl  7727  addnqpru  7728  recnnpr  7746  prmuloc2  7765  1idpru  7789  ltexprlemm  7798  ltexprlemloc  7805  recexprlemm  7822  recexprlem1ssl  7831  caucvgprlemnkj  7864  caucvgprlemnbj  7865  caucvgprlemm  7866  caucvgprlemopl  7867  caucvgprlemlol  7868  caucvgprlemladdfu  7875  caucvgprlemladdrl  7876  caucvgprprlemk  7881  caucvgprprlemloccalc  7882  caucvgprprlemnkltj  7887  caucvgprprlemnjltk  7889  caucvgprprlemml  7892  caucvgprprlemmu  7893  caucvgprprlemlol  7896  caucvgprprlemexb  7905  caucvgprprlem1  7907  suplocexprlemml  7914  suplocexprlemlub  7922  addclsr  7951  mulclsr  7952  prsrcl  7982  caucvgsrlemoffcau  7996  peano5nnnn  8090  mulap0r  8773  nn1suc  9140  prime  9557  zindd  9576  xrlttri3  10005  xnn0xadd0  10075  fzopth  10269  fzsuc  10277  fzpred  10278  fzp1ss  10281  fztp  10286  fseq1p1m1  10302  1fv  10347  elfzom1elp1fzo  10420  ssfzo12  10442  fzosplitsn  10451  zsupcllemstep  10461  zsupcllemex  10462  infssuzledc  10466  divfl0  10528  fldiv4lem1div2uz2  10538  modqid  10583  modqmuladdim  10601  frecuzrdgtcl  10646  frecuzrdgfunlem  10653  frecfzennn  10660  frecfzen2  10661  seq3val  10694  seqvalcd  10695  seqsplitg  10723  iseqf1olemqcl  10733  iseqf1olemnab  10735  iseqf1olemmo  10739  iseqf1olemqk  10741  seq3f1olemstep  10748  seqf1oglem2  10754  seq3id3  10758  seqhomog  10764  faclbnd  10975  faclbnd3  10977  bcm1k  10994  hashfz1  11017  hashfz  11056  hashfzp1  11059  fiubm  11063  hashfacen  11071  leisorel  11072  wrdexb  11096  wrdsymb  11112  wrdred1hash  11128  lsw0  11132  lswex  11136  ccat0  11144  ccatval2  11146  ccats1val2  11187  swrds1  11216  swrdlsw  11217  ccats1pfxeqrex  11263  pfxccatin12lem1  11276  swrdccatin2  11277  swrdccat  11283  cats1fvd  11314  cjcj  11410  caucvgre  11508  r19.2uz  11520  resqrexlemgt0  11547  ltabs  11614  xrmaxiflemab  11774  xrmaxiflemlub  11775  nnf1o  11903  summodclem2a  11908  fsumf1o  11917  fisum0diag2  11974  modfsummodlemstep  11984  fsumparts  11997  clim2prod  12066  prodfap0  12072  prodmodclem2a  12103  fprodssdc  12117  fprodcllem  12133  ef0lem  12187  resinval  12242  recosval  12243  demoivreALT  12301  nn0o  12434  gcdmultiplez  12558  dvdssq  12568  nninfct  12578  eucalg  12597  lcmgcdnn  12620  dvdsnprmd  12663  prm2orodd  12664  isprm5lem  12679  qnumdenbi  12730  nn0gcdsq  12738  phibnd  12755  hashdvds  12759  phimullem  12763  prmdiveq  12774  hashgcdlem  12776  modprm0  12793  nnnn0modprm0  12794  modprmn0modprm0  12795  oddprm  12798  prm23lt5  12802  pcprendvds  12829  pcidlem  12862  pcmpt  12882  pcfac  12889  infpnlem2  12899  prmunb  12901  1arith  12906  4sqlem19  12948  unennn  12984  ennnfonelemk  12987  ennnfonelemjn  12989  ennnfonelemhf1o  13000  ennnfonelemex  13001  ennnfonelemf1  13005  ennnfonelemrn  13006  qnnen  13018  unbendc  13041  setsfun0  13084  srngbased  13196  srngplusgd  13197  srngmulrd  13198  srnginvld  13199  lmodbased  13214  lmodplusgd  13215  lmodscad  13216  lmodvscad  13217  ipsbased  13226  ipsaddgd  13227  ipsmulrd  13228  ipsscad  13229  ipsvscad  13230  ipsipd  13231  tgval  13311  prdsbas3  13336  isnsgrp  13455  ismnd  13468  dfgrp2e  13577  subgintm  13751  eqg0el  13782  ecqusaddcl  13792  kerf1ghm  13827  gsumfzconst  13894  imasrng  13935  srgisid  13965  srg1zr  13966  qusring2  14045  oppr1g  14061  dvdsr02  14085  isunitd  14086  crngunit  14091  unitpropdg  14128  elrhmunit  14157  subrngintm  14192  subrguss  14216  subrgunit  14219  subrgugrp  14220  subrgintm  14223  lmodfopnelem1  14304  rmodislmodlem  14330  rmodislmod  14331  lssuni  14343  islss3  14359  lss0v  14410  sraval  14417  rnglidlmmgm  14476  2idllidld  14486  2idlridld  14487  rng2idl0  14499  rng2idlsubg0  14502  zrh0  14605  znle  14617  zndvds0  14630  znf1o  14631  znleval  14633  znfi  14635  znhash  14636  znunit  14639  psrbasg  14654  psradd  14659  psr0cl  14661  mpladd  14684  cldval  14789  ntrfval  14790  clsfval  14791  neifval  14830  neif  14831  neival  14833  cnclima  14913  cncnpi  14918  cnrest2  14926  cnrest2r  14927  cnptoprest  14929  cnpdis  14932  txvalex  14944  txval  14945  txcnmpt  14963  txdis  14967  cnmpt1t  14975  cnmpt2t  14983  hmeocnv  14997  hmeontr  15003  txhmeo  15009  xmetunirn  15048  xmettpos  15060  metn0  15068  xmetres  15072  metres  15073  blrnps  15101  blrn  15102  blin2  15122  blbas  15123  xmeterval  15125  xmettxlem  15199  xmettx  15200  metcnpi  15205  reldvg  15369  dvaddxx  15393  dvmulxx  15394  dviaddf  15395  dvimulf  15396  dvfre  15400  dvmptid  15406  dveflem  15416  elply2  15425  plyreres  15454  sinq12gt0  15520  rprelogbdiv  15647  logbgcd1irr  15657  fsumdvdsmul  15681  lgslem4  15698  lgsdirprm  15729  gausslemma2dlem0a  15744  gausslemma2dlem0f  15749  gausslemma2dlem0i  15752  gausslemma2dlem1a  15753  gausslemma2dlem1cl  15754  gausslemma2dlem5  15761  gausslemma2dlem6  15762  gausslemma2d  15764  lgseisenlem1  15765  lgseisenlem2  15766  lgseisenlem3  15767  lgseisen  15769  lgsquadlem1  15772  m1lgs  15780  2lgslem1a  15783  2lgslem1c  15785  2lgsoddprmlem2  15801  edgstruct  15880  umgrnloopv  15930  umgredgprv  15931  upgr1edc  15937  umgredgne  15964  usgredgssen  15976  umgr2edg1  16023  uspgredg2vlem  16034  wlkm  16085  wlkvtxiedg  16091  wlkvtxiedgg  16092  wlk1walkdom  16105  g0wlk0  16116  wlkres  16123  trlf1  16131  trlreslem  16132  trlres  16133  clwwlkg  16136  clwwlkccatlem  16143  bj-inex  16353  bj-sucexg  16368  bj-peano4  16401  setindis  16413  bdsetindis  16415  bj-inf2vnlem1  16416  nnsf  16459  nninfall  16463  nninfsellemeq  16468  sbthom  16482