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 )

This proof depends on syntax axioms:   -> wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  4syl  18  simpl2im  390  hbim  1598  nfal  1629  19.9hd  1714  equsexd  1782  sbcof2  1863  aev  1865  sbequi  1892  nfsbd  2037  mo2n  2114  eupickb  2168  r19.29af2  2691  spc2gv  2916  spc3gv  2918  eqvincg  2950  sbcco3g  3205  ssrmof  3311  exmidsssnc  4340  exmid1stab  4345  snelpwi  4351  opth1  4376  frind  4497  onin  4531  abnexg  4592  reusv1  4604  xpexg  4889  reldmm  5000  dmexg  5046  rnexg  5047  elrelimasn  5153  relfld  5316  funimaexglem  5464  funimaexg  5465  fabexg  5579  fsnd  5684  elfvm  5729  nfvres  5732  funimass4  5753  elfvmptrab1  5801  funconstss  5827  f1oresrab  5873  resfunexg  5936  f1eqcocnv  5997  isores1  6020  isoini  6024  isose  6027  isopolem  6028  isosolem  6030  eusvobj2  6071  acexmidlemcase  6080  oprabid  6117  offval  6310  resfunexgALT  6337  offval3  6367  1stvalg  6376  2ndvalg  6377  1stcof  6397  2ndcof  6398  cnvf1o  6461  tposf12  6540  smores3  6564  smoiso  6573  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemssrecs  6610  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemssrecs  6623  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemres  6633  rdgss  6654  nnsucsssuc  6765  nntr2  6776  swoord1  6836  swoord2  6837  iinerm  6881  eroveu  6900  pmresg  6957  en1uniel  7091  dom1o  7116  pw2f1odclem  7134  fopwdom  7136  xpen  7145  mapunen  7151  ssenen  7152  isinfinf  7201  ac6sfi  7202  preimaf1ofi  7268  sbthlem1  7274  fczfsuppd  7297  fi0  7309  fiss  7311  supubti  7340  suplubti  7341  isotilem  7347  supisolem  7349  supisoex  7350  supisoti  7351  ordiso2  7376  eldju1st  7412  eldju2ndl  7413  updjud  7423  djudom  7434  ctmlemr  7449  enumctlemm  7455  nnnninfeq  7469  ctssexmid  7491  nninfwlpoimlemginf  7517  exmidonfinlem  7546  en2other2  7549  exmidaclem  7565  cc2lem  7633  cc3  7635  addclnq  7743  mulclnq  7744  1qec  7756  prarloclemarch2  7787  enq0tr  7802  addclnq0  7819  mulclnq0  7820  nq0m0r  7824  prarloclemlo  7862  prarloc  7871  genpml  7885  genpmu  7886  addnqprl  7897  addnqpru  7898  recnnpr  7916  prmuloc2  7935  1idpru  7959  ltexprlemm  7968  ltexprlemloc  7975  recexprlemm  7992  recexprlem1ssl  8001  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprprlemk  8051  caucvgprprlemloccalc  8052  caucvgprprlemnkltj  8057  caucvgprprlemnjltk  8059  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemlol  8066  caucvgprprlemexb  8075  caucvgprprlem1  8077  suplocexprlemml  8084  suplocexprlemlub  8092  addclsr  8121  mulclsr  8122  prsrcl  8152  caucvgsrlemoffcau  8166  peano5nnnn  8260  mulap0r  8946  indv  9298  nn1suc  9326  prime  9750  zindd  9769  xrlttri3  10210  xnn0xadd0  10280  fzopth  10478  fzsuc  10486  fzpred  10488  fzp1ss  10491  fztp  10496  fseq1p1m1  10512  1fv  10557  elfzom1elp1fzo  10631  ssfzo12  10653  fzosplitsn  10662  zsupcllemstep  10673  zsupcllemex  10674  infssuzledc  10678  divfl0  10746  fldiv4lem1div2uz2  10756  modqid  10801  modqmuladdim  10819  frecuzrdgtcl  10864  frecuzrdgfunlem  10871  frecfzennn  10878  frecfzen2  10879  seq3val  10912  seqvalcd  10913  seqsplitg  10941  iseqf1olemqcl  10951  iseqf1olemnab  10953  iseqf1olemmo  10957  iseqf1olemqk  10959  seq3f1olemstep  10966  seqf1oglem2  10972  seq3id3  10976  seqhomog  10982  faclbnd  11195  faclbnd3  11197  bcm1k  11214  hashfz1  11238  hashfz  11278  hashfzp1  11281  fiubm  11287  hashfacen  11300  leisorel  11305  wrdexb  11332  wrdsymb  11348  wrdred1hash  11364  lsw0  11368  lswex  11372  ccat0  11380  ccatval2  11382  ccatw2s1leng  11422  ccats1val2  11424  swrds1  11456  swrdlsw  11457  ccats1pfxeqrex  11503  pfxccatin12lem1  11516  swrdccatin2  11517  swrdccat  11523  cats1fvd  11554  s1s2d  11582  s1s3d  11583  cjcj  11664  caucvgre  11763  r19.2uz  11775  resqrexlemgt0  11802  ltabs  11870  xrmaxiflemab  12032  xrmaxiflemlub  12033  nnf1o  12162  summodclem2a  12167  fsumf1o  12176  fisum0diag2  12233  modfsummodlemstep  12243  fsumparts  12256  clim2prod  12325  prodfap0  12331  prodmodclem2a  12362  fprodssdc  12376  fprodcllem  12392  ef0lem  12446  resinval  12501  recosval  12502  demoivreALT  12560  nn0o  12693  gcdmultiplez  12817  dvdssq  12827  nninfct  12837  eucalg  12856  lcmgcdnn  12879  dvdsnprmd  12922  prm2orodd  12923  isprm5lem  12939  qnumdenbi  12991  nn0gcdsq  12999  phibnd  13018  hashdvds  13022  phimullem  13026  prmdiveq  13037  hashgcdlem  13039  modprm0  13056  nnnn0modprm0  13057  modprmn0modprm0  13058  oddprm  13061  prm23lt5  13065  pcprendvds  13092  pcidlem  13125  pcmpt  13145  pcfac  13152  infpnlem2  13162  prmunb  13164  1arith  13169  4sqlem19  13211  ballotfilemfp1  13283  ballotfilemic  13302  ballotfilem1c  13303  ballotfilemsima  13311  ballotfilemrv  13315  ballotfilemro  13318  ballotfilemfrc  13322  ballotfilemfrci  13323  ballotfilemfrceq  13324  ballotfilemfrcn0  13325  ballotfilemrinv0  13328  unennn  13340  ennnfonelemk  13343  ennnfonelemjn  13345  ennnfonelemhf1o  13356  ennnfonelemex  13357  ennnfonelemf1  13361  ennnfonelemrn  13362  qnnen  13374  unbendc  13397  setsfun0  13440  srngbased  13554  srngplusgd  13555  srngmulrd  13556  srnginvld  13557  lmodbased  13572  lmodplusgd  13573  lmodscad  13574  lmodvscad  13575  ipsbased  13584  ipsaddgd  13585  ipsmulrd  13586  ipsscad  13587  ipsvscad  13588  ipsipd  13589  tgval  13669  gzsumval2  13767  isnsgrp  13774  ismnd  13785  dfgrp2e  13886  subgintm  14054  eqg0el  14085  ecqusaddcl  14095  kerf1ghm  14130  gzsumconst  14227  gsumvalfi  14236  gsumf1ofi  14244  prdsbas3  14271  imasrng  14339  srgisid  14374  qusring2  14455  oppr1g  14472  dvdsr02  14496  isunitd  14497  crngunit  14502  unitpropdg  14539  elrhmunit  14568  subrngintm  14604  subrguss  14628  subrgunit  14631  subrgugrp  14632  subrgintm  14635  drngunz  14702  lmodfopnelem1  14745  rmodislmodlem  14771  rmodislmod  14772  lssuni  14784  islss3  14800  lss0v  14851  sraval  14858  rnglidlmmgm  14917  2idllidld  14927  2idlridld  14928  rng2idl0  14940  rng2idlsubg0  14943  zrh0  15044  znle  15056  zndvds0  15069  znf1o  15070  znleval  15072  znfi  15074  znhash  15075  znunit  15078  issubassa  15097  asclfval  15105  ascl0  15111  ascl1  15112  rnasclsubrg  15120  psrbaglecl  15144  psrbasg  15150  psradd  15155  psr0cl  15163  mpladd  15186  cldval  15291  ntrfval  15292  clsfval  15293  neifval  15332  neif  15333  neival  15335  cnclima  15415  cncnpi  15420  cnrest2  15428  cnrest2r  15429  cnptoprest  15431  cnpdis  15434  txvalex  15446  txval  15447  txcnmpt  15465  txdis  15469  cnmpt1t  15477  cnmpt2t  15485  hmeocnv  15499  hmeontr  15505  txhmeo  15511  xmetunirn  15550  xmettpos  15562  metn0  15570  xmetres  15574  metres  15575  blrnps  15603  blrn  15604  blin2  15624  blbas  15625  xmeterval  15627  xmettxlem  15701  xmettx  15702  metcnpi  15707  reldvg  15871  dvaddxx  15895  dvmulxx  15896  dviaddf  15897  dvimulf  15898  dvfre  15902  dvmptid  15908  dveflem  15918  elply2  15927  plyreres  15956  sinq12gt0  16023  logfac  16090  rprelogbdiv  16154  logbgcd1irr  16164  birthdaylem3  16188  ppinprm  16221  chtnprm  16223  ppiqp1le  16228  fsumdvdsmul  16246  bcmono  16265  bposlem1  16272  bposlem3  16274  bposlem5  16276  lgslem4  16288  lgsdirprm  16319  gausslemma2dlem0a  16334  gausslemma2dlem0f  16339  gausslemma2dlem0i  16342  gausslemma2dlem1a  16343  gausslemma2dlem1cl  16344  gausslemma2dlem5  16351  gausslemma2dlem6  16352  gausslemma2d  16354  lgseisenlem1  16355  lgseisenlem2  16356  lgseisenlem3  16357  lgseisen  16359  lgsquadlem1  16362  m1lgs  16370  2lgslem1a  16373  2lgslem1c  16375  2lgsoddprmlem2  16391  edgval  16467  edgstruct  16471  umgrnloopv  16521  umgredgprv  16522  upgr1edc  16528  umgredgne  16557  usgredgssen  16569  umgr2edg1  16616  uspgredg2vlem  16627  uspgr1edc  16647  uhgrspansubgrlem  16683  wlkm  16746  wlkvtxiedg  16752  wlkvtxiedgg  16753  wlk1walkdom  16766  g0wlk0  16777  wlkres  16786  trlf1  16795  trlreslem  16796  trlres  16797  clwwlkg  16800  clwwlkccatlem  16807  clwwlknon  16836  eupthfi  16858  eupthseg  16859  eupthres  16864  trlsegvdeglem1  16867  trlsegvdeglem7  16873  trlsegvdegfi  16874  eupth2lem3lem2fi  16876  eupth2lem3lem3fi  16877  eupth2lem3lem6fi  16878  eupth2lem3lem4fi  16880  eupth2lem3lem7fi  16881  eupth2lem3fi  16883  eupth2lemsfi  16885  eupth2fi  16886  konigsbergssiedgwen  16893  bj-inex  17099  bj-sucexg  17114  bj-peano4  17147  setindis  17159  bdsetindis  17161  bj-inf2vnlem1  17162  wexmiddiffilem  17209  wexmiddifxy  17212  nnsf  17214  nninfall  17218  nninfsellemeq  17223  sbthom  17237