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  1593  nfal  1624  19.9hd  1710  equsexd  1777  sbcof2  1858  aev  1860  sbequi  1887  nfsbd  2030  mo2n  2107  eupickb  2161  r19.29af2  2673  spc2gv  2897  spc3gv  2899  eqvincg  2930  sbcco3g  3185  ssrmof  3290  exmidsssnc  4293  exmid1stab  4298  snelpwi  4303  opth1  4328  frind  4449  onin  4483  abnexg  4543  reusv1  4555  xpexg  4840  reldmm  4950  dmexg  4996  rnexg  4997  elrelimasn  5102  relfld  5265  funimaexglem  5413  funimaexg  5414  fabexg  5524  fsnd  5628  elfvm  5672  nfvres  5675  funimass4  5696  elfvmptrab1  5741  funconstss  5765  f1oresrab  5812  resfunexg  5874  f1eqcocnv  5931  isores1  5954  isoini  5958  isose  5961  isopolem  5962  isosolem  5964  eusvobj2  6003  acexmidlemcase  6012  oprabid  6049  offval  6242  resfunexgALT  6269  offval3  6295  1stvalg  6304  2ndvalg  6305  1stcof  6325  2ndcof  6326  cnvf1o  6389  tposf12  6434  smores3  6458  smoiso  6467  tfr0dm  6487  tfrlemibxssdm  6492  tfrlemi14d  6498  tfrexlem  6499  tfr1onlemssrecs  6504  tfr1onlemsucfn  6505  tfr1onlemsucaccv  6506  tfr1onlembxssdm  6508  tfr1onlemres  6514  tfri1dALT  6516  tfrcllemssrecs  6517  tfrcllemsucfn  6518  tfrcllemsucaccv  6519  tfrcllembxssdm  6521  tfrcllemres  6527  rdgss  6548  nnsucsssuc  6659  nntr2  6670  swoord1  6730  swoord2  6731  iinerm  6775  eroveu  6794  pmresg  6844  en1uniel  6977  dom1o  7001  pw2f1odclem  7019  fopwdom  7021  xpen  7030  ssenen  7036  isinfinf  7085  ac6sfi  7086  preimaf1ofi  7149  sbthlem1  7155  fi0  7173  fiss  7175  supubti  7197  suplubti  7198  isotilem  7204  supisolem  7206  supisoex  7207  supisoti  7208  ordiso2  7233  eldju1st  7269  eldju2ndl  7270  updjud  7280  djudom  7291  ctmlemr  7306  enumctlemm  7312  nnnninfeq  7326  ctssexmid  7348  nninfwlpoimlemginf  7374  exmidonfinlem  7403  en2other2  7406  exmidaclem  7422  cc2lem  7484  cc3  7486  addclnq  7594  mulclnq  7595  1qec  7607  prarloclemarch2  7638  enq0tr  7653  addclnq0  7670  mulclnq0  7671  nq0m0r  7675  prarloclemlo  7713  prarloc  7722  genpml  7736  genpmu  7737  addnqprl  7748  addnqpru  7749  recnnpr  7767  prmuloc2  7786  1idpru  7810  ltexprlemm  7819  ltexprlemloc  7826  recexprlemm  7843  recexprlem1ssl  7852  caucvgprlemnkj  7885  caucvgprlemnbj  7886  caucvgprlemm  7887  caucvgprlemopl  7888  caucvgprlemlol  7889  caucvgprlemladdfu  7896  caucvgprlemladdrl  7897  caucvgprprlemk  7902  caucvgprprlemloccalc  7903  caucvgprprlemnkltj  7908  caucvgprprlemnjltk  7910  caucvgprprlemml  7913  caucvgprprlemmu  7914  caucvgprprlemlol  7917  caucvgprprlemexb  7926  caucvgprprlem1  7928  suplocexprlemml  7935  suplocexprlemlub  7943  addclsr  7972  mulclsr  7973  prsrcl  8003  caucvgsrlemoffcau  8017  peano5nnnn  8111  mulap0r  8794  nn1suc  9161  prime  9578  zindd  9597  xrlttri3  10031  xnn0xadd0  10101  fzopth  10295  fzsuc  10303  fzpred  10304  fzp1ss  10307  fztp  10312  fseq1p1m1  10328  1fv  10373  elfzom1elp1fzo  10446  ssfzo12  10468  fzosplitsn  10477  zsupcllemstep  10488  zsupcllemex  10489  infssuzledc  10493  divfl0  10555  fldiv4lem1div2uz2  10565  modqid  10610  modqmuladdim  10628  frecuzrdgtcl  10673  frecuzrdgfunlem  10680  frecfzennn  10687  frecfzen2  10688  seq3val  10721  seqvalcd  10722  seqsplitg  10750  iseqf1olemqcl  10760  iseqf1olemnab  10762  iseqf1olemmo  10766  iseqf1olemqk  10768  seq3f1olemstep  10775  seqf1oglem2  10781  seq3id3  10785  seqhomog  10791  faclbnd  11002  faclbnd3  11004  bcm1k  11021  hashfz1  11044  hashfz  11084  hashfzp1  11087  fiubm  11091  hashfacen  11099  leisorel  11100  wrdexb  11124  wrdsymb  11140  wrdred1hash  11156  lsw0  11160  lswex  11164  ccat0  11172  ccatval2  11174  ccatw2s1leng  11214  ccats1val2  11216  swrds1  11248  swrdlsw  11249  ccats1pfxeqrex  11295  pfxccatin12lem1  11308  swrdccatin2  11309  swrdccat  11315  cats1fvd  11346  cjcj  11443  caucvgre  11541  r19.2uz  11553  resqrexlemgt0  11580  ltabs  11647  xrmaxiflemab  11807  xrmaxiflemlub  11808  nnf1o  11936  summodclem2a  11941  fsumf1o  11950  fisum0diag2  12007  modfsummodlemstep  12017  fsumparts  12030  clim2prod  12099  prodfap0  12105  prodmodclem2a  12136  fprodssdc  12150  fprodcllem  12166  ef0lem  12220  resinval  12275  recosval  12276  demoivreALT  12334  nn0o  12467  gcdmultiplez  12591  dvdssq  12601  nninfct  12611  eucalg  12630  lcmgcdnn  12653  dvdsnprmd  12696  prm2orodd  12697  isprm5lem  12712  qnumdenbi  12763  nn0gcdsq  12771  phibnd  12788  hashdvds  12792  phimullem  12796  prmdiveq  12807  hashgcdlem  12809  modprm0  12826  nnnn0modprm0  12827  modprmn0modprm0  12828  oddprm  12831  prm23lt5  12835  pcprendvds  12862  pcidlem  12895  pcmpt  12915  pcfac  12922  infpnlem2  12932  prmunb  12934  1arith  12939  4sqlem19  12981  unennn  13017  ennnfonelemk  13020  ennnfonelemjn  13022  ennnfonelemhf1o  13033  ennnfonelemex  13034  ennnfonelemf1  13038  ennnfonelemrn  13039  qnnen  13051  unbendc  13074  setsfun0  13117  srngbased  13229  srngplusgd  13230  srngmulrd  13231  srnginvld  13232  lmodbased  13247  lmodplusgd  13248  lmodscad  13249  lmodvscad  13250  ipsbased  13259  ipsaddgd  13260  ipsmulrd  13261  ipsscad  13262  ipsvscad  13263  ipsipd  13264  tgval  13344  prdsbas3  13369  isnsgrp  13488  ismnd  13501  dfgrp2e  13610  subgintm  13784  eqg0el  13815  ecqusaddcl  13825  kerf1ghm  13860  gsumfzconst  13927  imasrng  13968  srgisid  13998  srg1zr  13999  qusring2  14078  oppr1g  14094  dvdsr02  14118  isunitd  14119  crngunit  14124  unitpropdg  14161  elrhmunit  14190  subrngintm  14225  subrguss  14249  subrgunit  14252  subrgugrp  14253  subrgintm  14256  lmodfopnelem1  14337  rmodislmodlem  14363  rmodislmod  14364  lssuni  14376  islss3  14392  lss0v  14443  sraval  14450  rnglidlmmgm  14509  2idllidld  14519  2idlridld  14520  rng2idl0  14532  rng2idlsubg0  14535  zrh0  14638  znle  14650  zndvds0  14663  znf1o  14664  znleval  14666  znfi  14668  znhash  14669  znunit  14672  psrbasg  14687  psradd  14692  psr0cl  14694  mpladd  14717  cldval  14822  ntrfval  14823  clsfval  14824  neifval  14863  neif  14864  neival  14866  cnclima  14946  cncnpi  14951  cnrest2  14959  cnrest2r  14960  cnptoprest  14962  cnpdis  14965  txvalex  14977  txval  14978  txcnmpt  14996  txdis  15000  cnmpt1t  15008  cnmpt2t  15016  hmeocnv  15030  hmeontr  15036  txhmeo  15042  xmetunirn  15081  xmettpos  15093  metn0  15101  xmetres  15105  metres  15106  blrnps  15134  blrn  15135  blin2  15155  blbas  15156  xmeterval  15158  xmettxlem  15232  xmettx  15233  metcnpi  15238  reldvg  15402  dvaddxx  15426  dvmulxx  15427  dviaddf  15428  dvimulf  15429  dvfre  15433  dvmptid  15439  dveflem  15449  elply2  15458  plyreres  15487  sinq12gt0  15553  rprelogbdiv  15680  logbgcd1irr  15690  fsumdvdsmul  15714  lgslem4  15731  lgsdirprm  15762  gausslemma2dlem0a  15777  gausslemma2dlem0f  15782  gausslemma2dlem0i  15785  gausslemma2dlem1a  15786  gausslemma2dlem1cl  15787  gausslemma2dlem5  15794  gausslemma2dlem6  15795  gausslemma2d  15797  lgseisenlem1  15798  lgseisenlem2  15799  lgseisenlem3  15800  lgseisen  15802  lgsquadlem1  15805  m1lgs  15813  2lgslem1a  15816  2lgslem1c  15818  2lgsoddprmlem2  15834  edgval  15910  edgstruct  15914  umgrnloopv  15964  umgredgprv  15965  upgr1edc  15971  umgredgne  16000  usgredgssen  16012  umgr2edg1  16059  uspgredg2vlem  16070  uspgr1edc  16090  uhgrspansubgrlem  16126  wlkm  16189  wlkvtxiedg  16195  wlkvtxiedgg  16196  wlk1walkdom  16209  g0wlk0  16220  wlkres  16229  trlf1  16238  trlreslem  16239  trlres  16240  clwwlkg  16243  clwwlkccatlem  16250  clwwlknon  16279  eupthfi  16301  eupthseg  16302  eupthres  16307  trlsegvdeglem1  16310  trlsegvdeglem7  16316  bj-inex  16502  bj-sucexg  16517  bj-peano4  16550  setindis  16562  bdsetindis  16564  bj-inf2vnlem1  16565  nnsf  16607  nninfall  16611  nninfsellemeq  16616  sbthom  16630  gfsumval  16680