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  384  hbim  1533  nfal  1564  19.9hd  1650  equsexd  1717  sbcof2  1798  aev  1800  sbequi  1827  nfsbd  1965  mo2n  2042  eupickb  2095  r19.29af2  2605  spc2gv  2816  spc3gv  2818  eqvincg  2849  sbcco3g  3101  ssrmof  3204  exmidsssnc  4181  snelpwi  4189  opth1  4213  frind  4329  onin  4363  abnexg  4423  reusv1  4435  xpexg  4717  dmexg  4867  rnexg  4868  relfld  5131  funimaexglem  5270  funimaexg  5271  fabexg  5374  fsnd  5474  nfvres  5518  funimass4  5536  elfvmptrab1  5579  funconstss  5602  f1oresrab  5649  resfunexg  5705  f1eqcocnv  5758  isores1  5781  isoini  5785  isose  5788  isopolem  5789  isosolem  5791  eusvobj2  5827  acexmidlemcase  5836  oprabid  5870  offval  6056  resfunexgALT  6075  offval3  6099  1stvalg  6107  2ndvalg  6108  1stcof  6128  2ndcof  6129  cnvf1o  6189  tposf12  6233  smores3  6257  smoiso  6266  tfr0dm  6286  tfrlemibxssdm  6291  tfrlemi14d  6297  tfrexlem  6298  tfr1onlemssrecs  6303  tfr1onlemsucfn  6304  tfr1onlemsucaccv  6305  tfr1onlembxssdm  6307  tfr1onlemres  6313  tfri1dALT  6315  tfrcllemssrecs  6316  tfrcllemsucfn  6317  tfrcllemsucaccv  6318  tfrcllembxssdm  6320  tfrcllemres  6326  rdgss  6347  nnsucsssuc  6456  nntr2  6467  swoord1  6526  swoord2  6527  iinerm  6569  eroveu  6588  pmresg  6638  en1uniel  6766  fopwdom  6798  xpen  6807  ssenen  6813  isinfinf  6859  ac6sfi  6860  preimaf1ofi  6912  sbthlem1  6918  fi0  6936  fiss  6938  supubti  6960  suplubti  6961  isotilem  6967  supisolem  6969  supisoex  6970  supisoti  6971  ordiso2  6996  eldju1st  7032  eldju2ndl  7033  updjud  7043  djudom  7054  ctmlemr  7069  enumctlemm  7075  nnnninfeq  7088  ctssexmid  7110  exmidonfinlem  7145  en2other2  7148  exmidaclem  7160  cc2lem  7203  cc3  7205  addclnq  7312  mulclnq  7313  1qec  7325  prarloclemarch2  7356  enq0tr  7371  addclnq0  7388  mulclnq0  7389  nq0m0r  7393  prarloclemlo  7431  prarloc  7440  genpml  7454  genpmu  7455  addnqprl  7466  addnqpru  7467  recnnpr  7485  prmuloc2  7504  1idpru  7528  ltexprlemm  7537  ltexprlemloc  7544  recexprlemm  7561  recexprlem1ssl  7570  caucvgprlemnkj  7603  caucvgprlemnbj  7604  caucvgprlemm  7605  caucvgprlemopl  7606  caucvgprlemlol  7607  caucvgprlemladdfu  7614  caucvgprlemladdrl  7615  caucvgprprlemk  7620  caucvgprprlemloccalc  7621  caucvgprprlemnkltj  7626  caucvgprprlemnjltk  7628  caucvgprprlemml  7631  caucvgprprlemmu  7632  caucvgprprlemlol  7635  caucvgprprlemexb  7644  caucvgprprlem1  7646  suplocexprlemml  7653  suplocexprlemlub  7661  addclsr  7690  mulclsr  7691  prsrcl  7721  caucvgsrlemoffcau  7735  peano5nnnn  7829  mulap0r  8509  nn1suc  8872  prime  9286  zindd  9305  xrlttri3  9729  xnn0xadd0  9799  fzopth  9992  fzsuc  10000  fzpred  10001  fzp1ss  10004  fztp  10009  fseq1p1m1  10025  1fv  10070  elfzom1elp1fzo  10133  ssfzo12  10155  fzosplitsn  10164  divfl0  10227  modqid  10280  modqmuladdim  10298  frecuzrdgtcl  10343  frecuzrdgfunlem  10350  frecfzennn  10357  frecfzen2  10358  seq3val  10389  seqvalcd  10390  iseqf1olemqcl  10417  iseqf1olemnab  10419  iseqf1olemmo  10423  iseqf1olemqk  10425  seq3f1olemstep  10432  seq3id3  10438  faclbnd  10650  faclbnd3  10652  bcm1k  10669  hashfz1  10692  focdmex  10696  hashfz  10730  hashfzp1  10733  fiubm  10737  hashfacen  10745  leisorel  10746  cjcj  10821  caucvgre  10919  r19.2uz  10931  resqrexlemgt0  10958  ltabs  11025  xrmaxiflemab  11184  xrmaxiflemlub  11185  nnf1o  11313  summodclem2a  11318  fsumf1o  11327  fisum0diag2  11384  modfsummodlemstep  11394  fsumparts  11407  clim2prod  11476  prodfap0  11482  prodmodclem2a  11513  fprodssdc  11527  fprodcllem  11543  ef0lem  11597  resinval  11652  recosval  11653  demoivreALT  11710  nn0o  11840  zsupcllemstep  11874  zsupcllemex  11875  infssuzledc  11879  gcdmultiplez  11950  dvdssq  11960  eucalg  11987  lcmgcdnn  12010  dvdsnprmd  12053  prm2orodd  12054  isprm5lem  12069  qnumdenbi  12120  nn0gcdsq  12128  phibnd  12145  hashdvds  12149  phimullem  12153  prmdiveq  12164  hashgcdlem  12166  modprm0  12182  nnnn0modprm0  12183  modprmn0modprm0  12184  oddprm  12187  prm23lt5  12191  pcprendvds  12218  pcidlem  12250  pcmpt  12269  pcfac  12276  infpnlem2  12286  prmunb  12288  1arith  12293  unennn  12326  ennnfonelemk  12329  ennnfonelemjn  12331  ennnfonelemhf1o  12342  ennnfonelemex  12343  ennnfonelemf1  12347  ennnfonelemrn  12348  qnnen  12360  unbendc  12383  setsfun0  12426  srngbased  12513  srngplusgd  12514  srngmulrd  12515  srnginvld  12516  lmodbased  12524  lmodplusgd  12525  lmodscad  12526  lmodvscad  12527  ipsbased  12532  ipsaddgd  12533  ipsmulrd  12534  ipsscad  12535  ipsvscad  12536  ipsipd  12537  tgval  12649  cldval  12699  ntrfval  12700  clsfval  12701  neifval  12740  neif  12741  neival  12743  cnclima  12823  cncnpi  12828  cnrest2  12836  cnrest2r  12837  cnptoprest  12839  cnpdis  12842  txvalex  12854  txval  12855  txcnmpt  12873  txdis  12877  cnmpt1t  12885  cnmpt2t  12893  hmeocnv  12907  hmeontr  12913  txhmeo  12919  xmetunirn  12958  xmettpos  12970  metn0  12978  xmetres  12982  metres  12983  blrnps  13011  blrn  13012  blin2  13032  blbas  13033  xmeterval  13035  xmettxlem  13109  xmettx  13110  metcnpi  13115  reldvg  13248  dvaddxx  13267  dvmulxx  13268  dviaddf  13269  dvimulf  13270  dvfre  13274  dveflem  13287  sinq12gt0  13351  rprelogbdiv  13475  logbgcd1irr  13485  lgslem4  13504  lgsdirprm  13535  bj-inex  13749  bj-sucexg  13764  bj-peano4  13797  setindis  13809  bdsetindis  13811  bj-inf2vnlem1  13812  exmid1stab  13840  nnsf  13845  nninfall  13849  nninfsellemeq  13854  sbthom  13865