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  1569  nfal  1600  19.9hd  1686  equsexd  1753  sbcof2  1834  aev  1836  sbequi  1863  nfsbd  2006  mo2n  2083  eupickb  2137  r19.29af2  2648  spc2gv  2871  spc3gv  2873  eqvincg  2904  sbcco3g  3159  ssrmof  3264  exmidsssnc  4263  exmid1stab  4268  snelpwi  4273  opth1  4298  frind  4417  onin  4451  abnexg  4511  reusv1  4523  xpexg  4807  dmexg  4961  rnexg  4962  elrelimasn  5067  relfld  5230  funimaexglem  5376  funimaexg  5377  fabexg  5485  fsnd  5588  elfvm  5632  nfvres  5633  funimass4  5652  elfvmptrab1  5697  funconstss  5721  f1oresrab  5768  resfunexg  5828  f1eqcocnv  5883  isores1  5906  isoini  5910  isose  5913  isopolem  5914  isosolem  5916  eusvobj2  5953  acexmidlemcase  5962  oprabid  5999  offval  6189  resfunexgALT  6216  offval3  6242  1stvalg  6251  2ndvalg  6252  1stcof  6272  2ndcof  6273  cnvf1o  6334  tposf12  6378  smores3  6402  smoiso  6411  tfr0dm  6431  tfrlemibxssdm  6436  tfrlemi14d  6442  tfrexlem  6443  tfr1onlemssrecs  6448  tfr1onlemsucfn  6449  tfr1onlemsucaccv  6450  tfr1onlembxssdm  6452  tfr1onlemres  6458  tfri1dALT  6460  tfrcllemssrecs  6461  tfrcllemsucfn  6462  tfrcllemsucaccv  6463  tfrcllembxssdm  6465  tfrcllemres  6471  rdgss  6492  nnsucsssuc  6601  nntr2  6612  swoord1  6672  swoord2  6673  iinerm  6717  eroveu  6736  pmresg  6786  en1uniel  6919  pw2f1odclem  6956  fopwdom  6958  xpen  6967  ssenen  6973  isinfinf  7020  ac6sfi  7021  preimaf1ofi  7079  sbthlem1  7085  fi0  7103  fiss  7105  supubti  7127  suplubti  7128  isotilem  7134  supisolem  7136  supisoex  7137  supisoti  7138  ordiso2  7163  eldju1st  7199  eldju2ndl  7200  updjud  7210  djudom  7221  ctmlemr  7236  enumctlemm  7242  nnnninfeq  7256  ctssexmid  7278  nninfwlpoimlemginf  7304  exmidonfinlem  7332  en2other2  7335  exmidaclem  7351  cc2lem  7413  cc3  7415  addclnq  7523  mulclnq  7524  1qec  7536  prarloclemarch2  7567  enq0tr  7582  addclnq0  7599  mulclnq0  7600  nq0m0r  7604  prarloclemlo  7642  prarloc  7651  genpml  7665  genpmu  7666  addnqprl  7677  addnqpru  7678  recnnpr  7696  prmuloc2  7715  1idpru  7739  ltexprlemm  7748  ltexprlemloc  7755  recexprlemm  7772  recexprlem1ssl  7781  caucvgprlemnkj  7814  caucvgprlemnbj  7815  caucvgprlemm  7816  caucvgprlemopl  7817  caucvgprlemlol  7818  caucvgprlemladdfu  7825  caucvgprlemladdrl  7826  caucvgprprlemk  7831  caucvgprprlemloccalc  7832  caucvgprprlemnkltj  7837  caucvgprprlemnjltk  7839  caucvgprprlemml  7842  caucvgprprlemmu  7843  caucvgprprlemlol  7846  caucvgprprlemexb  7855  caucvgprprlem1  7857  suplocexprlemml  7864  suplocexprlemlub  7872  addclsr  7901  mulclsr  7902  prsrcl  7932  caucvgsrlemoffcau  7946  peano5nnnn  8040  mulap0r  8723  nn1suc  9090  prime  9507  zindd  9526  xrlttri3  9954  xnn0xadd0  10024  fzopth  10218  fzsuc  10226  fzpred  10227  fzp1ss  10230  fztp  10235  fseq1p1m1  10251  1fv  10296  elfzom1elp1fzo  10368  ssfzo12  10390  fzosplitsn  10399  zsupcllemstep  10409  zsupcllemex  10410  infssuzledc  10414  divfl0  10476  fldiv4lem1div2uz2  10486  modqid  10531  modqmuladdim  10549  frecuzrdgtcl  10594  frecuzrdgfunlem  10601  frecfzennn  10608  frecfzen2  10609  seq3val  10642  seqvalcd  10643  seqsplitg  10671  iseqf1olemqcl  10681  iseqf1olemnab  10683  iseqf1olemmo  10687  iseqf1olemqk  10689  seq3f1olemstep  10696  seqf1oglem2  10702  seq3id3  10706  seqhomog  10712  faclbnd  10923  faclbnd3  10925  bcm1k  10942  hashfz1  10965  hashfz  11003  hashfzp1  11006  fiubm  11010  hashfacen  11018  leisorel  11019  wrdexb  11043  wrdsymb  11058  wrdred1hash  11074  lsw0  11078  lswex  11082  ccat0  11090  ccatval2  11092  ccats1val2  11130  swrds1  11159  swrdlsw  11160  ccats1pfxeqrex  11206  pfxccatin12lem1  11219  swrdccatin2  11220  swrdccat  11226  cjcj  11309  caucvgre  11407  r19.2uz  11419  resqrexlemgt0  11446  ltabs  11513  xrmaxiflemab  11673  xrmaxiflemlub  11674  nnf1o  11802  summodclem2a  11807  fsumf1o  11816  fisum0diag2  11873  modfsummodlemstep  11883  fsumparts  11896  clim2prod  11965  prodfap0  11971  prodmodclem2a  12002  fprodssdc  12016  fprodcllem  12032  ef0lem  12086  resinval  12141  recosval  12142  demoivreALT  12200  nn0o  12333  gcdmultiplez  12457  dvdssq  12467  nninfct  12477  eucalg  12496  lcmgcdnn  12519  dvdsnprmd  12562  prm2orodd  12563  isprm5lem  12578  qnumdenbi  12629  nn0gcdsq  12637  phibnd  12654  hashdvds  12658  phimullem  12662  prmdiveq  12673  hashgcdlem  12675  modprm0  12692  nnnn0modprm0  12693  modprmn0modprm0  12694  oddprm  12697  prm23lt5  12701  pcprendvds  12728  pcidlem  12761  pcmpt  12781  pcfac  12788  infpnlem2  12798  prmunb  12800  1arith  12805  4sqlem19  12847  unennn  12883  ennnfonelemk  12886  ennnfonelemjn  12888  ennnfonelemhf1o  12899  ennnfonelemex  12900  ennnfonelemf1  12904  ennnfonelemrn  12905  qnnen  12917  unbendc  12940  setsfun0  12983  srngbased  13094  srngplusgd  13095  srngmulrd  13096  srnginvld  13097  lmodbased  13112  lmodplusgd  13113  lmodscad  13114  lmodvscad  13115  ipsbased  13124  ipsaddgd  13125  ipsmulrd  13126  ipsscad  13127  ipsvscad  13128  ipsipd  13129  tgval  13209  prdsbas3  13234  isnsgrp  13353  ismnd  13366  dfgrp2e  13475  subgintm  13649  eqg0el  13680  ecqusaddcl  13690  kerf1ghm  13725  gsumfzconst  13792  imasrng  13833  srgisid  13863  srg1zr  13864  qusring2  13943  oppr1g  13959  dvdsr02  13982  isunitd  13983  crngunit  13988  unitpropdg  14025  elrhmunit  14054  subrngintm  14089  subrguss  14113  subrgunit  14116  subrgugrp  14117  subrgintm  14120  lmodfopnelem1  14201  rmodislmodlem  14227  rmodislmod  14228  lssuni  14240  islss3  14256  lss0v  14307  sraval  14314  rnglidlmmgm  14373  2idllidld  14383  2idlridld  14384  rng2idl0  14396  rng2idlsubg0  14399  zrh0  14502  znle  14514  zndvds0  14527  znf1o  14528  znleval  14530  znfi  14532  znhash  14533  znunit  14536  psrbasg  14551  psradd  14556  psr0cl  14558  mpladd  14581  cldval  14686  ntrfval  14687  clsfval  14688  neifval  14727  neif  14728  neival  14730  cnclima  14810  cncnpi  14815  cnrest2  14823  cnrest2r  14824  cnptoprest  14826  cnpdis  14829  txvalex  14841  txval  14842  txcnmpt  14860  txdis  14864  cnmpt1t  14872  cnmpt2t  14880  hmeocnv  14894  hmeontr  14900  txhmeo  14906  xmetunirn  14945  xmettpos  14957  metn0  14965  xmetres  14969  metres  14970  blrnps  14998  blrn  14999  blin2  15019  blbas  15020  xmeterval  15022  xmettxlem  15096  xmettx  15097  metcnpi  15102  reldvg  15266  dvaddxx  15290  dvmulxx  15291  dviaddf  15292  dvimulf  15293  dvfre  15297  dvmptid  15303  dveflem  15313  elply2  15322  plyreres  15351  sinq12gt0  15417  rprelogbdiv  15544  logbgcd1irr  15554  fsumdvdsmul  15578  lgslem4  15595  lgsdirprm  15626  gausslemma2dlem0a  15641  gausslemma2dlem0f  15646  gausslemma2dlem0i  15649  gausslemma2dlem1a  15650  gausslemma2dlem1cl  15651  gausslemma2dlem5  15658  gausslemma2dlem6  15659  gausslemma2d  15661  lgseisenlem1  15662  lgseisenlem2  15663  lgseisenlem3  15664  lgseisen  15666  lgsquadlem1  15669  m1lgs  15677  2lgslem1a  15680  2lgslem1c  15682  2lgsoddprmlem2  15698  edgstruct  15775  umgrnloopvv  15825  upgr1edc  15829  umgredgne  15854  bj-inex  16042  bj-sucexg  16057  bj-peano4  16090  setindis  16102  bdsetindis  16104  bj-inf2vnlem1  16105  dom1o  16128  nnsf  16144  nninfall  16148  nninfsellemeq  16153  sbthom  16167