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  7274  en2other2  7277  exmidaclem  7293  cc2lem  7351  cc3  7353  addclnq  7461  mulclnq  7462  1qec  7474  prarloclemarch2  7505  enq0tr  7520  addclnq0  7537  mulclnq0  7538  nq0m0r  7542  prarloclemlo  7580  prarloc  7589  genpml  7603  genpmu  7604  addnqprl  7615  addnqpru  7616  recnnpr  7634  prmuloc2  7653  1idpru  7677  ltexprlemm  7686  ltexprlemloc  7693  recexprlemm  7710  recexprlem1ssl  7719  caucvgprlemnkj  7752  caucvgprlemnbj  7753  caucvgprlemm  7754  caucvgprlemopl  7755  caucvgprlemlol  7756  caucvgprlemladdfu  7763  caucvgprlemladdrl  7764  caucvgprprlemk  7769  caucvgprprlemloccalc  7770  caucvgprprlemnkltj  7775  caucvgprprlemnjltk  7777  caucvgprprlemml  7780  caucvgprprlemmu  7781  caucvgprprlemlol  7784  caucvgprprlemexb  7793  caucvgprprlem1  7795  suplocexprlemml  7802  suplocexprlemlub  7810  addclsr  7839  mulclsr  7840  prsrcl  7870  caucvgsrlemoffcau  7884  peano5nnnn  7978  mulap0r  8661  nn1suc  9028  prime  9444  zindd  9463  xrlttri3  9891  xnn0xadd0  9961  fzopth  10155  fzsuc  10163  fzpred  10164  fzp1ss  10167  fztp  10172  fseq1p1m1  10188  1fv  10233  elfzom1elp1fzo  10297  ssfzo12  10319  fzosplitsn  10328  zsupcllemstep  10338  zsupcllemex  10339  infssuzledc  10343  divfl0  10405  fldiv4lem1div2uz2  10415  modqid  10460  modqmuladdim  10478  frecuzrdgtcl  10523  frecuzrdgfunlem  10530  frecfzennn  10537  frecfzen2  10538  seq3val  10571  seqvalcd  10572  seqsplitg  10600  iseqf1olemqcl  10610  iseqf1olemnab  10612  iseqf1olemmo  10616  iseqf1olemqk  10618  seq3f1olemstep  10625  seqf1oglem2  10631  seq3id3  10635  seqhomog  10641  faclbnd  10852  faclbnd3  10854  bcm1k  10871  hashfz1  10894  hashfz  10932  hashfzp1  10935  fiubm  10939  hashfacen  10947  leisorel  10948  wrdexb  10966  wrdsymb  10981  wrdred1hash  10997  cjcj  11067  caucvgre  11165  r19.2uz  11177  resqrexlemgt0  11204  ltabs  11271  xrmaxiflemab  11431  xrmaxiflemlub  11432  nnf1o  11560  summodclem2a  11565  fsumf1o  11574  fisum0diag2  11631  modfsummodlemstep  11641  fsumparts  11654  clim2prod  11723  prodfap0  11729  prodmodclem2a  11760  fprodssdc  11774  fprodcllem  11790  ef0lem  11844  resinval  11899  recosval  11900  demoivreALT  11958  nn0o  12091  gcdmultiplez  12215  dvdssq  12225  nninfct  12235  eucalg  12254  lcmgcdnn  12277  dvdsnprmd  12320  prm2orodd  12321  isprm5lem  12336  qnumdenbi  12387  nn0gcdsq  12395  phibnd  12412  hashdvds  12416  phimullem  12420  prmdiveq  12431  hashgcdlem  12433  modprm0  12450  nnnn0modprm0  12451  modprmn0modprm0  12452  oddprm  12455  prm23lt5  12459  pcprendvds  12486  pcidlem  12519  pcmpt  12539  pcfac  12546  infpnlem2  12556  prmunb  12558  1arith  12563  4sqlem19  12605  unennn  12641  ennnfonelemk  12644  ennnfonelemjn  12646  ennnfonelemhf1o  12657  ennnfonelemex  12658  ennnfonelemf1  12662  ennnfonelemrn  12663  qnnen  12675  unbendc  12698  setsfun0  12741  srngbased  12851  srngplusgd  12852  srngmulrd  12853  srnginvld  12854  lmodbased  12869  lmodplusgd  12870  lmodscad  12871  lmodvscad  12872  ipsbased  12881  ipsaddgd  12882  ipsmulrd  12883  ipsscad  12884  ipsvscad  12885  ipsipd  12886  tgval  12966  prdsbas3  12991  isnsgrp  13110  ismnd  13123  dfgrp2e  13232  subgintm  13406  eqg0el  13437  ecqusaddcl  13447  kerf1ghm  13482  gsumfzconst  13549  imasrng  13590  srgisid  13620  srg1zr  13621  qusring2  13700  oppr1g  13716  dvdsr02  13739  isunitd  13740  crngunit  13745  unitpropdg  13782  elrhmunit  13811  subrngintm  13846  subrguss  13870  subrgunit  13873  subrgugrp  13874  subrgintm  13877  lmodfopnelem1  13958  rmodislmodlem  13984  rmodislmod  13985  lssuni  13997  islss3  14013  lss0v  14064  sraval  14071  rnglidlmmgm  14130  2idllidld  14140  2idlridld  14141  rng2idl0  14153  rng2idlsubg0  14156  zrh0  14259  znle  14271  zndvds0  14284  znf1o  14285  znleval  14287  znfi  14289  znhash  14290  znunit  14293  psrbasg  14308  psradd  14313  psr0cl  14315  mpladd  14338  cldval  14443  ntrfval  14444  clsfval  14445  neifval  14484  neif  14485  neival  14487  cnclima  14567  cncnpi  14572  cnrest2  14580  cnrest2r  14581  cnptoprest  14583  cnpdis  14586  txvalex  14598  txval  14599  txcnmpt  14617  txdis  14621  cnmpt1t  14629  cnmpt2t  14637  hmeocnv  14651  hmeontr  14657  txhmeo  14663  xmetunirn  14702  xmettpos  14714  metn0  14722  xmetres  14726  metres  14727  blrnps  14755  blrn  14756  blin2  14776  blbas  14777  xmeterval  14779  xmettxlem  14853  xmettx  14854  metcnpi  14859  reldvg  15023  dvaddxx  15047  dvmulxx  15048  dviaddf  15049  dvimulf  15050  dvfre  15054  dvmptid  15060  dveflem  15070  elply2  15079  plyreres  15108  sinq12gt0  15174  rprelogbdiv  15301  logbgcd1irr  15311  fsumdvdsmul  15335  lgslem4  15352  lgsdirprm  15383  gausslemma2dlem0a  15398  gausslemma2dlem0f  15403  gausslemma2dlem0i  15406  gausslemma2dlem1a  15407  gausslemma2dlem1cl  15408  gausslemma2dlem5  15415  gausslemma2dlem6  15416  gausslemma2d  15418  lgseisenlem1  15419  lgseisenlem2  15420  lgseisenlem3  15421  lgseisen  15423  lgsquadlem1  15426  m1lgs  15434  2lgslem1a  15437  2lgslem1c  15439  2lgsoddprmlem2  15455  bj-inex  15661  bj-sucexg  15676  bj-peano4  15709  setindis  15721  bdsetindis  15723  bj-inf2vnlem1  15724  nnsf  15760  nninfall  15764  nninfsellemeq  15769  sbthom  15783