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  1559  nfal  1590  19.9hd  1676  equsexd  1743  sbcof2  1824  aev  1826  sbequi  1853  nfsbd  1996  mo2n  2073  eupickb  2126  r19.29af2  2637  spc2gv  2855  spc3gv  2857  eqvincg  2888  sbcco3g  3142  ssrmof  3247  exmidsssnc  4237  exmid1stab  4242  snelpwi  4246  opth1  4270  frind  4388  onin  4422  abnexg  4482  reusv1  4494  xpexg  4778  dmexg  4931  rnexg  4932  elrelimasn  5036  relfld  5199  funimaexglem  5342  funimaexg  5343  fabexg  5448  fsnd  5550  elfvm  5594  nfvres  5595  funimass4  5614  elfvmptrab1  5659  funconstss  5683  f1oresrab  5730  resfunexg  5786  f1eqcocnv  5841  isores1  5864  isoini  5868  isose  5871  isopolem  5872  isosolem  5874  eusvobj2  5911  acexmidlemcase  5920  oprabid  5957  offval  6147  resfunexgALT  6174  offval3  6200  1stvalg  6209  2ndvalg  6210  1stcof  6230  2ndcof  6231  cnvf1o  6292  tposf12  6336  smores3  6360  smoiso  6369  tfr0dm  6389  tfrlemibxssdm  6394  tfrlemi14d  6400  tfrexlem  6401  tfr1onlemssrecs  6406  tfr1onlemsucfn  6407  tfr1onlemsucaccv  6408  tfr1onlembxssdm  6410  tfr1onlemres  6416  tfri1dALT  6418  tfrcllemssrecs  6419  tfrcllemsucfn  6420  tfrcllemsucaccv  6421  tfrcllembxssdm  6423  tfrcllemres  6429  rdgss  6450  nnsucsssuc  6559  nntr2  6570  swoord1  6630  swoord2  6631  iinerm  6675  eroveu  6694  pmresg  6744  en1uniel  6872  pw2f1odclem  6904  fopwdom  6906  xpen  6915  ssenen  6921  isinfinf  6967  ac6sfi  6968  preimaf1ofi  7026  sbthlem1  7032  fi0  7050  fiss  7052  supubti  7074  suplubti  7075  isotilem  7081  supisolem  7083  supisoex  7084  supisoti  7085  ordiso2  7110  eldju1st  7146  eldju2ndl  7147  updjud  7157  djudom  7168  ctmlemr  7183  enumctlemm  7189  nnnninfeq  7203  ctssexmid  7225  nninfwlpoimlemginf  7251  exmidonfinlem  7272  en2other2  7275  exmidaclem  7291  cc2lem  7349  cc3  7351  addclnq  7459  mulclnq  7460  1qec  7472  prarloclemarch2  7503  enq0tr  7518  addclnq0  7535  mulclnq0  7536  nq0m0r  7540  prarloclemlo  7578  prarloc  7587  genpml  7601  genpmu  7602  addnqprl  7613  addnqpru  7614  recnnpr  7632  prmuloc2  7651  1idpru  7675  ltexprlemm  7684  ltexprlemloc  7691  recexprlemm  7708  recexprlem1ssl  7717  caucvgprlemnkj  7750  caucvgprlemnbj  7751  caucvgprlemm  7752  caucvgprlemopl  7753  caucvgprlemlol  7754  caucvgprlemladdfu  7761  caucvgprlemladdrl  7762  caucvgprprlemk  7767  caucvgprprlemloccalc  7768  caucvgprprlemnkltj  7773  caucvgprprlemnjltk  7775  caucvgprprlemml  7778  caucvgprprlemmu  7779  caucvgprprlemlol  7782  caucvgprprlemexb  7791  caucvgprprlem1  7793  suplocexprlemml  7800  suplocexprlemlub  7808  addclsr  7837  mulclsr  7838  prsrcl  7868  caucvgsrlemoffcau  7882  peano5nnnn  7976  mulap0r  8659  nn1suc  9026  prime  9442  zindd  9461  xrlttri3  9889  xnn0xadd0  9959  fzopth  10153  fzsuc  10161  fzpred  10162  fzp1ss  10165  fztp  10170  fseq1p1m1  10186  1fv  10231  elfzom1elp1fzo  10295  ssfzo12  10317  fzosplitsn  10326  zsupcllemstep  10336  zsupcllemex  10337  infssuzledc  10341  divfl0  10403  fldiv4lem1div2uz2  10413  modqid  10458  modqmuladdim  10476  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  frecfzennn  10535  frecfzen2  10536  seq3val  10569  seqvalcd  10570  seqsplitg  10598  iseqf1olemqcl  10608  iseqf1olemnab  10610  iseqf1olemmo  10614  iseqf1olemqk  10616  seq3f1olemstep  10623  seqf1oglem2  10629  seq3id3  10633  seqhomog  10639  faclbnd  10850  faclbnd3  10852  bcm1k  10869  hashfz1  10892  hashfz  10930  hashfzp1  10933  fiubm  10937  hashfacen  10945  leisorel  10946  wrdexb  10964  wrdsymb  10979  wrdred1hash  10995  cjcj  11065  caucvgre  11163  r19.2uz  11175  resqrexlemgt0  11202  ltabs  11269  xrmaxiflemab  11429  xrmaxiflemlub  11430  nnf1o  11558  summodclem2a  11563  fsumf1o  11572  fisum0diag2  11629  modfsummodlemstep  11639  fsumparts  11652  clim2prod  11721  prodfap0  11727  prodmodclem2a  11758  fprodssdc  11772  fprodcllem  11788  ef0lem  11842  resinval  11897  recosval  11898  demoivreALT  11956  nn0o  12089  gcdmultiplez  12213  dvdssq  12223  nninfct  12233  eucalg  12252  lcmgcdnn  12275  dvdsnprmd  12318  prm2orodd  12319  isprm5lem  12334  qnumdenbi  12385  nn0gcdsq  12393  phibnd  12410  hashdvds  12414  phimullem  12418  prmdiveq  12429  hashgcdlem  12431  modprm0  12448  nnnn0modprm0  12449  modprmn0modprm0  12450  oddprm  12453  prm23lt5  12457  pcprendvds  12484  pcidlem  12517  pcmpt  12537  pcfac  12544  infpnlem2  12554  prmunb  12556  1arith  12561  4sqlem19  12603  unennn  12639  ennnfonelemk  12642  ennnfonelemjn  12644  ennnfonelemhf1o  12655  ennnfonelemex  12656  ennnfonelemf1  12660  ennnfonelemrn  12661  qnnen  12673  unbendc  12696  setsfun0  12739  srngbased  12849  srngplusgd  12850  srngmulrd  12851  srnginvld  12852  lmodbased  12867  lmodplusgd  12868  lmodscad  12869  lmodvscad  12870  ipsbased  12879  ipsaddgd  12880  ipsmulrd  12881  ipsscad  12882  ipsvscad  12883  ipsipd  12884  tgval  12964  prdsbas3  12989  isnsgrp  13108  ismnd  13121  dfgrp2e  13230  subgintm  13404  eqg0el  13435  ecqusaddcl  13445  kerf1ghm  13480  gsumfzconst  13547  imasrng  13588  srgisid  13618  srg1zr  13619  qusring2  13698  oppr1g  13714  dvdsr02  13737  isunitd  13738  crngunit  13743  unitpropdg  13780  elrhmunit  13809  subrngintm  13844  subrguss  13868  subrgunit  13871  subrgugrp  13872  subrgintm  13875  lmodfopnelem1  13956  rmodislmodlem  13982  rmodislmod  13983  lssuni  13995  islss3  14011  lss0v  14062  sraval  14069  rnglidlmmgm  14128  2idllidld  14138  2idlridld  14139  rng2idl0  14151  rng2idlsubg0  14154  zrh0  14257  znle  14269  zndvds0  14282  znf1o  14283  znleval  14285  znfi  14287  znhash  14288  znunit  14291  psrbasg  14303  psradd  14307  psr0cl  14309  cldval  14419  ntrfval  14420  clsfval  14421  neifval  14460  neif  14461  neival  14463  cnclima  14543  cncnpi  14548  cnrest2  14556  cnrest2r  14557  cnptoprest  14559  cnpdis  14562  txvalex  14574  txval  14575  txcnmpt  14593  txdis  14597  cnmpt1t  14605  cnmpt2t  14613  hmeocnv  14627  hmeontr  14633  txhmeo  14639  xmetunirn  14678  xmettpos  14690  metn0  14698  xmetres  14702  metres  14703  blrnps  14731  blrn  14732  blin2  14752  blbas  14753  xmeterval  14755  xmettxlem  14829  xmettx  14830  metcnpi  14835  reldvg  14999  dvaddxx  15023  dvmulxx  15024  dviaddf  15025  dvimulf  15026  dvfre  15030  dvmptid  15036  dveflem  15046  elply2  15055  plyreres  15084  sinq12gt0  15150  rprelogbdiv  15277  logbgcd1irr  15287  fsumdvdsmul  15311  lgslem4  15328  lgsdirprm  15359  gausslemma2dlem0a  15374  gausslemma2dlem0f  15379  gausslemma2dlem0i  15382  gausslemma2dlem1a  15383  gausslemma2dlem1cl  15384  gausslemma2dlem5  15391  gausslemma2dlem6  15392  gausslemma2d  15394  lgseisenlem1  15395  lgseisenlem2  15396  lgseisenlem3  15397  lgseisen  15399  lgsquadlem1  15402  m1lgs  15410  2lgslem1a  15413  2lgslem1c  15415  2lgsoddprmlem2  15431  bj-inex  15637  bj-sucexg  15652  bj-peano4  15685  setindis  15697  bdsetindis  15699  bj-inf2vnlem1  15700  nnsf  15736  nninfall  15740  nninfsellemeq  15745  sbthom  15757