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  4247  exmid1stab  4252  snelpwi  4256  opth1  4280  frind  4399  onin  4433  abnexg  4493  reusv1  4505  xpexg  4789  dmexg  4942  rnexg  4943  elrelimasn  5048  relfld  5211  funimaexglem  5357  funimaexg  5358  fabexg  5463  fsnd  5565  elfvm  5609  nfvres  5610  funimass4  5629  elfvmptrab1  5674  funconstss  5698  f1oresrab  5745  resfunexg  5805  f1eqcocnv  5860  isores1  5883  isoini  5887  isose  5890  isopolem  5891  isosolem  5893  eusvobj2  5930  acexmidlemcase  5939  oprabid  5976  offval  6166  resfunexgALT  6193  offval3  6219  1stvalg  6228  2ndvalg  6229  1stcof  6249  2ndcof  6250  cnvf1o  6311  tposf12  6355  smores3  6379  smoiso  6388  tfr0dm  6408  tfrlemibxssdm  6413  tfrlemi14d  6419  tfrexlem  6420  tfr1onlemssrecs  6425  tfr1onlemsucfn  6426  tfr1onlemsucaccv  6427  tfr1onlembxssdm  6429  tfr1onlemres  6435  tfri1dALT  6437  tfrcllemssrecs  6438  tfrcllemsucfn  6439  tfrcllemsucaccv  6440  tfrcllembxssdm  6442  tfrcllemres  6448  rdgss  6469  nnsucsssuc  6578  nntr2  6589  swoord1  6649  swoord2  6650  iinerm  6694  eroveu  6713  pmresg  6763  en1uniel  6896  pw2f1odclem  6931  fopwdom  6933  xpen  6942  ssenen  6948  isinfinf  6994  ac6sfi  6995  preimaf1ofi  7053  sbthlem1  7059  fi0  7077  fiss  7079  supubti  7101  suplubti  7102  isotilem  7108  supisolem  7110  supisoex  7111  supisoti  7112  ordiso2  7137  eldju1st  7173  eldju2ndl  7174  updjud  7184  djudom  7195  ctmlemr  7210  enumctlemm  7216  nnnninfeq  7230  ctssexmid  7252  nninfwlpoimlemginf  7278  exmidonfinlem  7301  en2other2  7304  exmidaclem  7320  cc2lem  7378  cc3  7380  addclnq  7488  mulclnq  7489  1qec  7501  prarloclemarch2  7532  enq0tr  7547  addclnq0  7564  mulclnq0  7565  nq0m0r  7569  prarloclemlo  7607  prarloc  7616  genpml  7630  genpmu  7631  addnqprl  7642  addnqpru  7643  recnnpr  7661  prmuloc2  7680  1idpru  7704  ltexprlemm  7713  ltexprlemloc  7720  recexprlemm  7737  recexprlem1ssl  7746  caucvgprlemnkj  7779  caucvgprlemnbj  7780  caucvgprlemm  7781  caucvgprlemopl  7782  caucvgprlemlol  7783  caucvgprlemladdfu  7790  caucvgprlemladdrl  7791  caucvgprprlemk  7796  caucvgprprlemloccalc  7797  caucvgprprlemnkltj  7802  caucvgprprlemnjltk  7804  caucvgprprlemml  7807  caucvgprprlemmu  7808  caucvgprprlemlol  7811  caucvgprprlemexb  7820  caucvgprprlem1  7822  suplocexprlemml  7829  suplocexprlemlub  7837  addclsr  7866  mulclsr  7867  prsrcl  7897  caucvgsrlemoffcau  7911  peano5nnnn  8005  mulap0r  8688  nn1suc  9055  prime  9472  zindd  9491  xrlttri3  9919  xnn0xadd0  9989  fzopth  10183  fzsuc  10191  fzpred  10192  fzp1ss  10195  fztp  10200  fseq1p1m1  10216  1fv  10261  elfzom1elp1fzo  10331  ssfzo12  10353  fzosplitsn  10362  zsupcllemstep  10372  zsupcllemex  10373  infssuzledc  10377  divfl0  10439  fldiv4lem1div2uz2  10449  modqid  10494  modqmuladdim  10512  frecuzrdgtcl  10557  frecuzrdgfunlem  10564  frecfzennn  10571  frecfzen2  10572  seq3val  10605  seqvalcd  10606  seqsplitg  10634  iseqf1olemqcl  10644  iseqf1olemnab  10646  iseqf1olemmo  10650  iseqf1olemqk  10652  seq3f1olemstep  10659  seqf1oglem2  10665  seq3id3  10669  seqhomog  10675  faclbnd  10886  faclbnd3  10888  bcm1k  10905  hashfz1  10928  hashfz  10966  hashfzp1  10969  fiubm  10973  hashfacen  10981  leisorel  10982  wrdexb  11006  wrdsymb  11021  wrdred1hash  11037  lsw0  11041  ccat0  11052  ccatval2  11054  ccats1val2  11092  swrds1  11121  swrdlsw  11122  cjcj  11194  caucvgre  11292  r19.2uz  11304  resqrexlemgt0  11331  ltabs  11398  xrmaxiflemab  11558  xrmaxiflemlub  11559  nnf1o  11687  summodclem2a  11692  fsumf1o  11701  fisum0diag2  11758  modfsummodlemstep  11768  fsumparts  11781  clim2prod  11850  prodfap0  11856  prodmodclem2a  11887  fprodssdc  11901  fprodcllem  11917  ef0lem  11971  resinval  12026  recosval  12027  demoivreALT  12085  nn0o  12218  gcdmultiplez  12342  dvdssq  12352  nninfct  12362  eucalg  12381  lcmgcdnn  12404  dvdsnprmd  12447  prm2orodd  12448  isprm5lem  12463  qnumdenbi  12514  nn0gcdsq  12522  phibnd  12539  hashdvds  12543  phimullem  12547  prmdiveq  12558  hashgcdlem  12560  modprm0  12577  nnnn0modprm0  12578  modprmn0modprm0  12579  oddprm  12582  prm23lt5  12586  pcprendvds  12613  pcidlem  12646  pcmpt  12666  pcfac  12673  infpnlem2  12683  prmunb  12685  1arith  12690  4sqlem19  12732  unennn  12768  ennnfonelemk  12771  ennnfonelemjn  12773  ennnfonelemhf1o  12784  ennnfonelemex  12785  ennnfonelemf1  12789  ennnfonelemrn  12790  qnnen  12802  unbendc  12825  setsfun0  12868  srngbased  12979  srngplusgd  12980  srngmulrd  12981  srnginvld  12982  lmodbased  12997  lmodplusgd  12998  lmodscad  12999  lmodvscad  13000  ipsbased  13009  ipsaddgd  13010  ipsmulrd  13011  ipsscad  13012  ipsvscad  13013  ipsipd  13014  tgval  13094  prdsbas3  13119  isnsgrp  13238  ismnd  13251  dfgrp2e  13360  subgintm  13534  eqg0el  13565  ecqusaddcl  13575  kerf1ghm  13610  gsumfzconst  13677  imasrng  13718  srgisid  13748  srg1zr  13749  qusring2  13828  oppr1g  13844  dvdsr02  13867  isunitd  13868  crngunit  13873  unitpropdg  13910  elrhmunit  13939  subrngintm  13974  subrguss  13998  subrgunit  14001  subrgugrp  14002  subrgintm  14005  lmodfopnelem1  14086  rmodislmodlem  14112  rmodislmod  14113  lssuni  14125  islss3  14141  lss0v  14192  sraval  14199  rnglidlmmgm  14258  2idllidld  14268  2idlridld  14269  rng2idl0  14281  rng2idlsubg0  14284  zrh0  14387  znle  14399  zndvds0  14412  znf1o  14413  znleval  14415  znfi  14417  znhash  14418  znunit  14421  psrbasg  14436  psradd  14441  psr0cl  14443  mpladd  14466  cldval  14571  ntrfval  14572  clsfval  14573  neifval  14612  neif  14613  neival  14615  cnclima  14695  cncnpi  14700  cnrest2  14708  cnrest2r  14709  cnptoprest  14711  cnpdis  14714  txvalex  14726  txval  14727  txcnmpt  14745  txdis  14749  cnmpt1t  14757  cnmpt2t  14765  hmeocnv  14779  hmeontr  14785  txhmeo  14791  xmetunirn  14830  xmettpos  14842  metn0  14850  xmetres  14854  metres  14855  blrnps  14883  blrn  14884  blin2  14904  blbas  14905  xmeterval  14907  xmettxlem  14981  xmettx  14982  metcnpi  14987  reldvg  15151  dvaddxx  15175  dvmulxx  15176  dviaddf  15177  dvimulf  15178  dvfre  15182  dvmptid  15188  dveflem  15198  elply2  15207  plyreres  15236  sinq12gt0  15302  rprelogbdiv  15429  logbgcd1irr  15439  fsumdvdsmul  15463  lgslem4  15480  lgsdirprm  15511  gausslemma2dlem0a  15526  gausslemma2dlem0f  15531  gausslemma2dlem0i  15534  gausslemma2dlem1a  15535  gausslemma2dlem1cl  15536  gausslemma2dlem5  15543  gausslemma2dlem6  15544  gausslemma2d  15546  lgseisenlem1  15547  lgseisenlem2  15548  lgseisenlem3  15549  lgseisen  15551  lgsquadlem1  15554  m1lgs  15562  2lgslem1a  15565  2lgslem1c  15567  2lgsoddprmlem2  15583  edgstruct  15656  bj-inex  15843  bj-sucexg  15858  bj-peano4  15891  setindis  15903  bdsetindis  15905  bj-inf2vnlem1  15906  nnsf  15942  nninfall  15946  nninfsellemeq  15951  sbthom  15965