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  5513  fsnd  5616  elfvm  5660  nfvres  5663  funimass4  5684  elfvmptrab1  5729  funconstss  5753  f1oresrab  5800  resfunexg  5860  f1eqcocnv  5915  isores1  5938  isoini  5942  isose  5945  isopolem  5946  isosolem  5948  eusvobj2  5987  acexmidlemcase  5996  oprabid  6033  offval  6226  resfunexgALT  6253  offval3  6279  1stvalg  6288  2ndvalg  6289  1stcof  6309  2ndcof  6310  cnvf1o  6371  tposf12  6415  smores3  6439  smoiso  6448  tfr0dm  6468  tfrlemibxssdm  6473  tfrlemi14d  6479  tfrexlem  6480  tfr1onlemssrecs  6485  tfr1onlemsucfn  6486  tfr1onlemsucaccv  6487  tfr1onlembxssdm  6489  tfr1onlemres  6495  tfri1dALT  6497  tfrcllemssrecs  6498  tfrcllemsucfn  6499  tfrcllemsucaccv  6500  tfrcllembxssdm  6502  tfrcllemres  6508  rdgss  6529  nnsucsssuc  6638  nntr2  6649  swoord1  6709  swoord2  6710  iinerm  6754  eroveu  6773  pmresg  6823  en1uniel  6956  dom1o  6977  pw2f1odclem  6995  fopwdom  6997  xpen  7006  ssenen  7012  isinfinf  7059  ac6sfi  7060  preimaf1ofi  7118  sbthlem1  7124  fi0  7142  fiss  7144  supubti  7166  suplubti  7167  isotilem  7173  supisolem  7175  supisoex  7176  supisoti  7177  ordiso2  7202  eldju1st  7238  eldju2ndl  7239  updjud  7249  djudom  7260  ctmlemr  7275  enumctlemm  7281  nnnninfeq  7295  ctssexmid  7317  nninfwlpoimlemginf  7343  exmidonfinlem  7371  en2other2  7374  exmidaclem  7390  cc2lem  7452  cc3  7454  addclnq  7562  mulclnq  7563  1qec  7575  prarloclemarch2  7606  enq0tr  7621  addclnq0  7638  mulclnq0  7639  nq0m0r  7643  prarloclemlo  7681  prarloc  7690  genpml  7704  genpmu  7705  addnqprl  7716  addnqpru  7717  recnnpr  7735  prmuloc2  7754  1idpru  7778  ltexprlemm  7787  ltexprlemloc  7794  recexprlemm  7811  recexprlem1ssl  7820  caucvgprlemnkj  7853  caucvgprlemnbj  7854  caucvgprlemm  7855  caucvgprlemopl  7856  caucvgprlemlol  7857  caucvgprlemladdfu  7864  caucvgprlemladdrl  7865  caucvgprprlemk  7870  caucvgprprlemloccalc  7871  caucvgprprlemnkltj  7876  caucvgprprlemnjltk  7878  caucvgprprlemml  7881  caucvgprprlemmu  7882  caucvgprprlemlol  7885  caucvgprprlemexb  7894  caucvgprprlem1  7896  suplocexprlemml  7903  suplocexprlemlub  7911  addclsr  7940  mulclsr  7941  prsrcl  7971  caucvgsrlemoffcau  7985  peano5nnnn  8079  mulap0r  8762  nn1suc  9129  prime  9546  zindd  9565  xrlttri3  9993  xnn0xadd0  10063  fzopth  10257  fzsuc  10265  fzpred  10266  fzp1ss  10269  fztp  10274  fseq1p1m1  10290  1fv  10335  elfzom1elp1fzo  10408  ssfzo12  10430  fzosplitsn  10439  zsupcllemstep  10449  zsupcllemex  10450  infssuzledc  10454  divfl0  10516  fldiv4lem1div2uz2  10526  modqid  10571  modqmuladdim  10589  frecuzrdgtcl  10634  frecuzrdgfunlem  10641  frecfzennn  10648  frecfzen2  10649  seq3val  10682  seqvalcd  10683  seqsplitg  10711  iseqf1olemqcl  10721  iseqf1olemnab  10723  iseqf1olemmo  10727  iseqf1olemqk  10729  seq3f1olemstep  10736  seqf1oglem2  10742  seq3id3  10746  seqhomog  10752  faclbnd  10963  faclbnd3  10965  bcm1k  10982  hashfz1  11005  hashfz  11043  hashfzp1  11046  fiubm  11050  hashfacen  11058  leisorel  11059  wrdexb  11083  wrdsymb  11099  wrdred1hash  11115  lsw0  11119  lswex  11123  ccat0  11131  ccatval2  11133  ccats1val2  11171  swrds1  11200  swrdlsw  11201  ccats1pfxeqrex  11247  pfxccatin12lem1  11260  swrdccatin2  11261  swrdccat  11267  cats1fvd  11298  cjcj  11394  caucvgre  11492  r19.2uz  11504  resqrexlemgt0  11531  ltabs  11598  xrmaxiflemab  11758  xrmaxiflemlub  11759  nnf1o  11887  summodclem2a  11892  fsumf1o  11901  fisum0diag2  11958  modfsummodlemstep  11968  fsumparts  11981  clim2prod  12050  prodfap0  12056  prodmodclem2a  12087  fprodssdc  12101  fprodcllem  12117  ef0lem  12171  resinval  12226  recosval  12227  demoivreALT  12285  nn0o  12418  gcdmultiplez  12542  dvdssq  12552  nninfct  12562  eucalg  12581  lcmgcdnn  12604  dvdsnprmd  12647  prm2orodd  12648  isprm5lem  12663  qnumdenbi  12714  nn0gcdsq  12722  phibnd  12739  hashdvds  12743  phimullem  12747  prmdiveq  12758  hashgcdlem  12760  modprm0  12777  nnnn0modprm0  12778  modprmn0modprm0  12779  oddprm  12782  prm23lt5  12786  pcprendvds  12813  pcidlem  12846  pcmpt  12866  pcfac  12873  infpnlem2  12883  prmunb  12885  1arith  12890  4sqlem19  12932  unennn  12968  ennnfonelemk  12971  ennnfonelemjn  12973  ennnfonelemhf1o  12984  ennnfonelemex  12985  ennnfonelemf1  12989  ennnfonelemrn  12990  qnnen  13002  unbendc  13025  setsfun0  13068  srngbased  13180  srngplusgd  13181  srngmulrd  13182  srnginvld  13183  lmodbased  13198  lmodplusgd  13199  lmodscad  13200  lmodvscad  13201  ipsbased  13210  ipsaddgd  13211  ipsmulrd  13212  ipsscad  13213  ipsvscad  13214  ipsipd  13215  tgval  13295  prdsbas3  13320  isnsgrp  13439  ismnd  13452  dfgrp2e  13561  subgintm  13735  eqg0el  13766  ecqusaddcl  13776  kerf1ghm  13811  gsumfzconst  13878  imasrng  13919  srgisid  13949  srg1zr  13950  qusring2  14029  oppr1g  14045  dvdsr02  14069  isunitd  14070  crngunit  14075  unitpropdg  14112  elrhmunit  14141  subrngintm  14176  subrguss  14200  subrgunit  14203  subrgugrp  14204  subrgintm  14207  lmodfopnelem1  14288  rmodislmodlem  14314  rmodislmod  14315  lssuni  14327  islss3  14343  lss0v  14394  sraval  14401  rnglidlmmgm  14460  2idllidld  14470  2idlridld  14471  rng2idl0  14483  rng2idlsubg0  14486  zrh0  14589  znle  14601  zndvds0  14614  znf1o  14615  znleval  14617  znfi  14619  znhash  14620  znunit  14623  psrbasg  14638  psradd  14643  psr0cl  14645  mpladd  14668  cldval  14773  ntrfval  14774  clsfval  14775  neifval  14814  neif  14815  neival  14817  cnclima  14897  cncnpi  14902  cnrest2  14910  cnrest2r  14911  cnptoprest  14913  cnpdis  14916  txvalex  14928  txval  14929  txcnmpt  14947  txdis  14951  cnmpt1t  14959  cnmpt2t  14967  hmeocnv  14981  hmeontr  14987  txhmeo  14993  xmetunirn  15032  xmettpos  15044  metn0  15052  xmetres  15056  metres  15057  blrnps  15085  blrn  15086  blin2  15106  blbas  15107  xmeterval  15109  xmettxlem  15183  xmettx  15184  metcnpi  15189  reldvg  15353  dvaddxx  15377  dvmulxx  15378  dviaddf  15379  dvimulf  15380  dvfre  15384  dvmptid  15390  dveflem  15400  elply2  15409  plyreres  15438  sinq12gt0  15504  rprelogbdiv  15631  logbgcd1irr  15641  fsumdvdsmul  15665  lgslem4  15682  lgsdirprm  15713  gausslemma2dlem0a  15728  gausslemma2dlem0f  15733  gausslemma2dlem0i  15736  gausslemma2dlem1a  15737  gausslemma2dlem1cl  15738  gausslemma2dlem5  15745  gausslemma2dlem6  15746  gausslemma2d  15748  lgseisenlem1  15749  lgseisenlem2  15750  lgseisenlem3  15751  lgseisen  15753  lgsquadlem1  15756  m1lgs  15764  2lgslem1a  15767  2lgslem1c  15769  2lgsoddprmlem2  15785  edgstruct  15864  umgrnloopv  15914  umgredgprv  15915  upgr1edc  15921  umgredgne  15948  usgredgssen  15960  umgr2edg1  16007  uspgredg2vlem  16018  wlkm  16051  wlkvtxiedg  16056  wlkvtxiedgg  16057  wlk1walkdom  16070  bj-inex  16270  bj-sucexg  16285  bj-peano4  16318  setindis  16330  bdsetindis  16332  bj-inf2vnlem1  16333  nnsf  16371  nninfall  16375  nninfsellemeq  16380  sbthom  16394