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  1556  nfal  1587  19.9hd  1673  equsexd  1740  sbcof2  1821  aev  1823  sbequi  1850  nfsbd  1993  mo2n  2070  eupickb  2123  r19.29af2  2634  spc2gv  2852  spc3gv  2854  eqvincg  2885  sbcco3g  3139  ssrmof  3243  exmidsssnc  4233  exmid1stab  4238  snelpwi  4242  opth1  4266  frind  4384  onin  4418  abnexg  4478  reusv1  4490  xpexg  4774  dmexg  4927  rnexg  4928  elrelimasn  5032  relfld  5195  funimaexglem  5338  funimaexg  5339  fabexg  5442  fsnd  5544  elfvm  5588  nfvres  5589  funimass4  5608  elfvmptrab1  5653  funconstss  5677  f1oresrab  5724  resfunexg  5780  f1eqcocnv  5835  isores1  5858  isoini  5862  isose  5865  isopolem  5866  isosolem  5868  eusvobj2  5905  acexmidlemcase  5914  oprabid  5951  offval  6140  resfunexgALT  6162  offval3  6188  1stvalg  6197  2ndvalg  6198  1stcof  6218  2ndcof  6219  cnvf1o  6280  tposf12  6324  smores3  6348  smoiso  6357  tfr0dm  6377  tfrlemibxssdm  6382  tfrlemi14d  6388  tfrexlem  6389  tfr1onlemssrecs  6394  tfr1onlemsucfn  6395  tfr1onlemsucaccv  6396  tfr1onlembxssdm  6398  tfr1onlemres  6404  tfri1dALT  6406  tfrcllemssrecs  6407  tfrcllemsucfn  6408  tfrcllemsucaccv  6409  tfrcllembxssdm  6411  tfrcllemres  6417  rdgss  6438  nnsucsssuc  6547  nntr2  6558  swoord1  6618  swoord2  6619  iinerm  6663  eroveu  6682  pmresg  6732  en1uniel  6860  pw2f1odclem  6892  fopwdom  6894  xpen  6903  ssenen  6909  isinfinf  6955  ac6sfi  6956  preimaf1ofi  7012  sbthlem1  7018  fi0  7036  fiss  7038  supubti  7060  suplubti  7061  isotilem  7067  supisolem  7069  supisoex  7070  supisoti  7071  ordiso2  7096  eldju1st  7132  eldju2ndl  7133  updjud  7143  djudom  7154  ctmlemr  7169  enumctlemm  7175  nnnninfeq  7189  ctssexmid  7211  nninfwlpoimlemginf  7237  exmidonfinlem  7255  en2other2  7258  exmidaclem  7270  cc2lem  7328  cc3  7330  addclnq  7437  mulclnq  7438  1qec  7450  prarloclemarch2  7481  enq0tr  7496  addclnq0  7513  mulclnq0  7514  nq0m0r  7518  prarloclemlo  7556  prarloc  7565  genpml  7579  genpmu  7580  addnqprl  7591  addnqpru  7592  recnnpr  7610  prmuloc2  7629  1idpru  7653  ltexprlemm  7662  ltexprlemloc  7669  recexprlemm  7686  recexprlem1ssl  7695  caucvgprlemnkj  7728  caucvgprlemnbj  7729  caucvgprlemm  7730  caucvgprlemopl  7731  caucvgprlemlol  7732  caucvgprlemladdfu  7739  caucvgprlemladdrl  7740  caucvgprprlemk  7745  caucvgprprlemloccalc  7746  caucvgprprlemnkltj  7751  caucvgprprlemnjltk  7753  caucvgprprlemml  7756  caucvgprprlemmu  7757  caucvgprprlemlol  7760  caucvgprprlemexb  7769  caucvgprprlem1  7771  suplocexprlemml  7778  suplocexprlemlub  7786  addclsr  7815  mulclsr  7816  prsrcl  7846  caucvgsrlemoffcau  7860  peano5nnnn  7954  mulap0r  8636  nn1suc  9003  prime  9419  zindd  9438  xrlttri3  9866  xnn0xadd0  9936  fzopth  10130  fzsuc  10138  fzpred  10139  fzp1ss  10142  fztp  10147  fseq1p1m1  10163  1fv  10208  elfzom1elp1fzo  10272  ssfzo12  10294  fzosplitsn  10303  divfl0  10368  fldiv4lem1div2uz2  10378  modqid  10423  modqmuladdim  10441  frecuzrdgtcl  10486  frecuzrdgfunlem  10493  frecfzennn  10500  frecfzen2  10501  seq3val  10534  seqvalcd  10535  seqsplitg  10563  iseqf1olemqcl  10573  iseqf1olemnab  10575  iseqf1olemmo  10579  iseqf1olemqk  10581  seq3f1olemstep  10588  seqf1oglem2  10594  seq3id3  10598  seqhomog  10604  faclbnd  10815  faclbnd3  10817  bcm1k  10834  hashfz1  10857  hashfz  10895  hashfzp1  10898  fiubm  10902  hashfacen  10910  leisorel  10911  wrdexb  10929  wrdsymb  10944  wrdred1hash  10960  cjcj  11030  caucvgre  11128  r19.2uz  11140  resqrexlemgt0  11167  ltabs  11234  xrmaxiflemab  11393  xrmaxiflemlub  11394  nnf1o  11522  summodclem2a  11527  fsumf1o  11536  fisum0diag2  11593  modfsummodlemstep  11603  fsumparts  11616  clim2prod  11685  prodfap0  11691  prodmodclem2a  11722  fprodssdc  11736  fprodcllem  11752  ef0lem  11806  resinval  11861  recosval  11862  demoivreALT  11920  nn0o  12051  zsupcllemstep  12085  zsupcllemex  12086  infssuzledc  12090  gcdmultiplez  12161  dvdssq  12171  nninfct  12181  eucalg  12200  lcmgcdnn  12223  dvdsnprmd  12266  prm2orodd  12267  isprm5lem  12282  qnumdenbi  12333  nn0gcdsq  12341  phibnd  12358  hashdvds  12362  phimullem  12366  prmdiveq  12377  hashgcdlem  12379  modprm0  12395  nnnn0modprm0  12396  modprmn0modprm0  12397  oddprm  12400  prm23lt5  12404  pcprendvds  12431  pcidlem  12464  pcmpt  12484  pcfac  12491  infpnlem2  12501  prmunb  12503  1arith  12508  4sqlem19  12550  unennn  12557  ennnfonelemk  12560  ennnfonelemjn  12562  ennnfonelemhf1o  12573  ennnfonelemex  12574  ennnfonelemf1  12578  ennnfonelemrn  12579  qnnen  12591  unbendc  12614  setsfun0  12657  srngbased  12767  srngplusgd  12768  srngmulrd  12769  srnginvld  12770  lmodbased  12785  lmodplusgd  12786  lmodscad  12787  lmodvscad  12788  ipsbased  12797  ipsaddgd  12798  ipsmulrd  12799  ipsscad  12800  ipsvscad  12801  ipsipd  12802  tgval  12876  isnsgrp  12992  ismnd  13003  dfgrp2e  13103  subgintm  13271  eqg0el  13302  ecqusaddcl  13312  kerf1ghm  13347  gsumfzconst  13414  imasrng  13455  srgisid  13485  srg1zr  13486  qusring2  13565  oppr1g  13581  dvdsr02  13604  isunitd  13605  crngunit  13610  unitpropdg  13647  elrhmunit  13676  subrngintm  13711  subrguss  13735  subrgunit  13738  subrgugrp  13739  subrgintm  13742  lmodfopnelem1  13823  rmodislmodlem  13849  rmodislmod  13850  lssuni  13862  islss3  13878  lss0v  13929  sraval  13936  rnglidlmmgm  13995  2idllidld  14005  2idlridld  14006  rng2idl0  14018  rng2idlsubg0  14021  zrh0  14124  znle  14136  zndvds0  14149  znf1o  14150  znleval  14152  znfi  14154  znhash  14155  znunit  14158  psrbasg  14170  psradd  14174  cldval  14278  ntrfval  14279  clsfval  14280  neifval  14319  neif  14320  neival  14322  cnclima  14402  cncnpi  14407  cnrest2  14415  cnrest2r  14416  cnptoprest  14418  cnpdis  14421  txvalex  14433  txval  14434  txcnmpt  14452  txdis  14456  cnmpt1t  14464  cnmpt2t  14472  hmeocnv  14486  hmeontr  14492  txhmeo  14498  xmetunirn  14537  xmettpos  14549  metn0  14557  xmetres  14561  metres  14562  blrnps  14590  blrn  14591  blin2  14611  blbas  14612  xmeterval  14614  xmettxlem  14688  xmettx  14689  metcnpi  14694  reldvg  14858  dvaddxx  14882  dvmulxx  14883  dviaddf  14884  dvimulf  14885  dvfre  14889  dvmptid  14895  dveflem  14905  elply2  14914  plyreres  14942  sinq12gt0  15006  rprelogbdiv  15130  logbgcd1irr  15140  lgslem4  15160  lgsdirprm  15191  gausslemma2dlem0a  15206  gausslemma2dlem0f  15211  gausslemma2dlem0i  15214  gausslemma2dlem1a  15215  gausslemma2dlem1cl  15216  gausslemma2dlem5  15223  gausslemma2dlem6  15224  gausslemma2d  15226  lgseisenlem1  15227  lgseisenlem2  15228  lgseisenlem3  15229  lgseisen  15231  lgsquadlem1  15234  m1lgs  15242  2lgslem1a  15245  2lgslem1c  15247  2lgsoddprmlem2  15263  bj-inex  15469  bj-sucexg  15484  bj-peano4  15517  setindis  15529  bdsetindis  15531  bj-inf2vnlem1  15532  nnsf  15565  nninfall  15569  nninfsellemeq  15574  sbthom  15586