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  1594  nfal  1625  19.9hd  1710  equsexd  1778  sbcof2  1859  aev  1861  sbequi  1888  nfsbd  2033  mo2n  2110  eupickb  2164  r19.29af2  2685  spc2gv  2910  spc3gv  2912  eqvincg  2944  sbcco3g  3199  ssrmof  3305  exmidsssnc  4321  exmid1stab  4326  snelpwi  4332  opth1  4357  frind  4478  onin  4512  abnexg  4572  reusv1  4584  xpexg  4869  reldmm  4980  dmexg  5026  rnexg  5027  elrelimasn  5133  relfld  5296  funimaexglem  5444  funimaexg  5445  fabexg  5559  fsnd  5664  elfvm  5708  nfvres  5711  funimass4  5732  elfvmptrab1  5777  funconstss  5801  f1oresrab  5847  resfunexg  5910  f1eqcocnv  5970  isores1  5993  isoini  5997  isose  6000  isopolem  6001  isosolem  6003  eusvobj2  6044  acexmidlemcase  6053  oprabid  6090  offval  6283  resfunexgALT  6310  offval3  6340  1stvalg  6349  2ndvalg  6350  1stcof  6370  2ndcof  6371  cnvf1o  6434  tposf12  6513  smores3  6537  smoiso  6546  tfr0dm  6566  tfrlemibxssdm  6571  tfrlemi14d  6577  tfrexlem  6578  tfr1onlemssrecs  6583  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlemres  6593  tfri1dALT  6595  tfrcllemssrecs  6596  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllemres  6606  rdgss  6627  nnsucsssuc  6738  nntr2  6749  swoord1  6809  swoord2  6810  iinerm  6854  eroveu  6873  pmresg  6923  en1uniel  7057  dom1o  7082  pw2f1odclem  7100  fopwdom  7102  xpen  7111  mapunen  7117  ssenen  7118  isinfinf  7167  ac6sfi  7168  preimaf1ofi  7234  sbthlem1  7240  fczfsuppd  7263  fi0  7275  fiss  7277  supubti  7303  suplubti  7304  isotilem  7310  supisolem  7312  supisoex  7313  supisoti  7314  ordiso2  7339  eldju1st  7375  eldju2ndl  7376  updjud  7386  djudom  7397  ctmlemr  7412  enumctlemm  7418  nnnninfeq  7432  ctssexmid  7454  nninfwlpoimlemginf  7480  exmidonfinlem  7509  en2other2  7512  exmidaclem  7528  cc2lem  7596  cc3  7598  addclnq  7706  mulclnq  7707  1qec  7719  prarloclemarch2  7750  enq0tr  7765  addclnq0  7782  mulclnq0  7783  nq0m0r  7787  prarloclemlo  7825  prarloc  7834  genpml  7848  genpmu  7849  addnqprl  7860  addnqpru  7861  recnnpr  7879  prmuloc2  7898  1idpru  7922  ltexprlemm  7931  ltexprlemloc  7938  recexprlemm  7955  recexprlem1ssl  7964  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprprlemk  8014  caucvgprprlemloccalc  8015  caucvgprprlemnkltj  8020  caucvgprprlemnjltk  8022  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemlol  8029  caucvgprprlemexb  8038  caucvgprprlem1  8040  suplocexprlemml  8047  suplocexprlemlub  8055  addclsr  8084  mulclsr  8085  prsrcl  8115  caucvgsrlemoffcau  8129  peano5nnnn  8223  mulap0r  8906  nn1suc  9273  prime  9695  zindd  9714  xrlttri3  10149  xnn0xadd0  10219  fzopth  10416  fzsuc  10424  fzpred  10426  fzp1ss  10429  fztp  10434  fseq1p1m1  10450  1fv  10495  elfzom1elp1fzo  10569  ssfzo12  10591  fzosplitsn  10600  zsupcllemstep  10611  zsupcllemex  10612  infssuzledc  10616  divfl0  10680  fldiv4lem1div2uz2  10690  modqid  10735  modqmuladdim  10753  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  frecfzennn  10812  frecfzen2  10813  seq3val  10846  seqvalcd  10847  seqsplitg  10875  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemmo  10891  iseqf1olemqk  10893  seq3f1olemstep  10900  seqf1oglem2  10906  seq3id3  10910  seqhomog  10916  faclbnd  11128  faclbnd3  11130  bcm1k  11147  hashfz1  11171  hashfz  11211  hashfzp1  11214  fiubm  11220  hashfacen  11233  leisorel  11234  wrdexb  11261  wrdsymb  11277  wrdred1hash  11293  lsw0  11297  lswex  11301  ccat0  11309  ccatval2  11311  ccatw2s1leng  11351  ccats1val2  11353  swrds1  11385  swrdlsw  11386  ccats1pfxeqrex  11432  pfxccatin12lem1  11445  swrdccatin2  11446  swrdccat  11452  cats1fvd  11483  s1s2d  11511  s1s3d  11512  cjcj  11593  caucvgre  11691  r19.2uz  11703  resqrexlemgt0  11730  ltabs  11797  xrmaxiflemab  11957  xrmaxiflemlub  11958  nnf1o  12087  summodclem2a  12092  fsumf1o  12101  fisum0diag2  12158  modfsummodlemstep  12168  fsumparts  12181  clim2prod  12250  prodfap0  12256  prodmodclem2a  12287  fprodssdc  12301  fprodcllem  12317  ef0lem  12371  resinval  12426  recosval  12427  demoivreALT  12485  nn0o  12618  gcdmultiplez  12742  dvdssq  12752  nninfct  12762  eucalg  12781  lcmgcdnn  12804  dvdsnprmd  12847  prm2orodd  12848  isprm5lem  12863  qnumdenbi  12914  nn0gcdsq  12922  phibnd  12939  hashdvds  12943  phimullem  12947  prmdiveq  12958  hashgcdlem  12960  modprm0  12977  nnnn0modprm0  12978  modprmn0modprm0  12979  oddprm  12982  prm23lt5  12986  pcprendvds  13013  pcidlem  13046  pcmpt  13066  pcfac  13073  infpnlem2  13083  prmunb  13085  1arith  13090  4sqlem19  13132  ballotfilemfp1  13175  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemsima  13203  ballotfilemrv  13207  ballotfilemro  13210  ballotfilemfrc  13214  ballotfilemfrci  13215  ballotfilemfrceq  13216  ballotfilemfrcn0  13217  ballotfilemrinv0  13220  unennn  13232  ennnfonelemk  13235  ennnfonelemjn  13237  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemf1  13253  ennnfonelemrn  13254  qnnen  13266  unbendc  13289  setsfun0  13332  srngbased  13444  srngplusgd  13445  srngmulrd  13446  srnginvld  13447  lmodbased  13462  lmodplusgd  13463  lmodscad  13464  lmodvscad  13465  ipsbased  13474  ipsaddgd  13475  ipsmulrd  13476  ipsscad  13477  ipsvscad  13478  ipsipd  13479  tgval  13559  isnsgrp  13669  ismnd  13680  dfgrp2e  13783  subgintm  13951  eqg0el  13982  ecqusaddcl  13992  kerf1ghm  14027  gsumfzconst  14094  gfsumval  14102  prdsbas3  14129  imasrng  14195  srgisid  14229  qusring2  14309  oppr1g  14326  dvdsr02  14350  isunitd  14351  crngunit  14356  unitpropdg  14393  elrhmunit  14422  subrngintm  14458  subrguss  14482  subrgunit  14485  subrgugrp  14486  subrgintm  14489  drngunz  14556  lmodfopnelem1  14598  rmodislmodlem  14624  rmodislmod  14625  lssuni  14637  islss3  14653  lss0v  14704  sraval  14711  rnglidlmmgm  14770  2idllidld  14780  2idlridld  14781  rng2idl0  14793  rng2idlsubg0  14796  zrh0  14899  znle  14911  zndvds0  14924  znf1o  14925  znleval  14927  znfi  14929  znhash  14930  znunit  14933  psrbaglecl  14950  psrbasg  14955  psradd  14960  psr0cl  14962  mpladd  14985  cldval  15090  ntrfval  15091  clsfval  15092  neifval  15131  neif  15132  neival  15134  cnclima  15214  cncnpi  15219  cnrest2  15227  cnrest2r  15228  cnptoprest  15230  cnpdis  15233  txvalex  15245  txval  15246  txcnmpt  15264  txdis  15268  cnmpt1t  15276  cnmpt2t  15284  hmeocnv  15298  hmeontr  15304  txhmeo  15310  xmetunirn  15349  xmettpos  15361  metn0  15369  xmetres  15373  metres  15374  blrnps  15402  blrn  15403  blin2  15423  blbas  15424  xmeterval  15426  xmettxlem  15500  xmettx  15501  metcnpi  15506  reldvg  15670  dvaddxx  15694  dvmulxx  15695  dviaddf  15696  dvimulf  15697  dvfre  15701  dvmptid  15707  dveflem  15717  elply2  15726  plyreres  15755  sinq12gt0  15821  rprelogbdiv  15948  logbgcd1irr  15958  fsumdvdsmul  15985  lgslem4  16002  lgsdirprm  16033  gausslemma2dlem0a  16048  gausslemma2dlem0f  16053  gausslemma2dlem0i  16056  gausslemma2dlem1a  16057  gausslemma2dlem1cl  16058  gausslemma2dlem5  16065  gausslemma2dlem6  16066  gausslemma2d  16068  lgseisenlem1  16069  lgseisenlem2  16070  lgseisenlem3  16071  lgseisen  16073  lgsquadlem1  16076  m1lgs  16084  2lgslem1a  16087  2lgslem1c  16089  2lgsoddprmlem2  16105  edgval  16181  edgstruct  16185  umgrnloopv  16235  umgredgprv  16236  upgr1edc  16242  umgredgne  16271  usgredgssen  16283  umgr2edg1  16330  uspgredg2vlem  16341  uspgr1edc  16361  uhgrspansubgrlem  16397  wlkm  16460  wlkvtxiedg  16466  wlkvtxiedgg  16467  wlk1walkdom  16480  g0wlk0  16491  wlkres  16500  trlf1  16509  trlreslem  16510  trlres  16511  clwwlkg  16514  clwwlkccatlem  16521  clwwlknon  16550  eupthfi  16572  eupthseg  16573  eupthres  16578  trlsegvdeglem1  16581  trlsegvdeglem7  16587  trlsegvdegfi  16588  eupth2lem3lem2fi  16590  eupth2lem3lem3fi  16591  eupth2lem3lem6fi  16592  eupth2lem3lem4fi  16594  eupth2lem3lem7fi  16595  eupth2lem3fi  16597  eupth2lemsfi  16599  eupth2fi  16600  konigsbergssiedgwen  16607  bj-inex  16803  bj-sucexg  16818  bj-peano4  16851  setindis  16863  bdsetindis  16865  bj-inf2vnlem1  16866  nnsf  16909  nninfall  16913  nninfsellemeq  16918  sbthom  16932