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  7339  suplubti  7340  isotilem  7346  supisolem  7348  supisoex  7349  supisoti  7350  ordiso2  7375  eldju1st  7411  eldju2ndl  7412  updjud  7422  djudom  7433  ctmlemr  7448  enumctlemm  7454  nnnninfeq  7468  ctssexmid  7490  nninfwlpoimlemginf  7516  exmidonfinlem  7545  en2other2  7548  exmidaclem  7564  cc2lem  7632  cc3  7634  addclnq  7742  mulclnq  7743  1qec  7755  prarloclemarch2  7786  enq0tr  7801  addclnq0  7818  mulclnq0  7819  nq0m0r  7823  prarloclemlo  7861  prarloc  7870  genpml  7884  genpmu  7885  addnqprl  7896  addnqpru  7897  recnnpr  7915  prmuloc2  7934  1idpru  7958  ltexprlemm  7967  ltexprlemloc  7974  recexprlemm  7991  recexprlem1ssl  8000  caucvgprlemnkj  8033  caucvgprlemnbj  8034  caucvgprlemm  8035  caucvgprlemopl  8036  caucvgprlemlol  8037  caucvgprlemladdfu  8044  caucvgprlemladdrl  8045  caucvgprprlemk  8050  caucvgprprlemloccalc  8051  caucvgprprlemnkltj  8056  caucvgprprlemnjltk  8058  caucvgprprlemml  8061  caucvgprprlemmu  8062  caucvgprprlemlol  8065  caucvgprprlemexb  8074  caucvgprprlem1  8076  suplocexprlemml  8083  suplocexprlemlub  8091  addclsr  8120  mulclsr  8121  prsrcl  8151  caucvgsrlemoffcau  8165  peano5nnnn  8259  mulap0r  8943  indv  9295  nn1suc  9323  prime  9745  zindd  9764  xrlttri3  10199  xnn0xadd0  10269  fzopth  10467  fzsuc  10475  fzpred  10477  fzp1ss  10480  fztp  10485  fseq1p1m1  10501  1fv  10546  elfzom1elp1fzo  10620  ssfzo12  10642  fzosplitsn  10651  zsupcllemstep  10662  zsupcllemex  10663  infssuzledc  10667  divfl0  10731  fldiv4lem1div2uz2  10741  modqid  10786  modqmuladdim  10804  frecuzrdgtcl  10849  frecuzrdgfunlem  10856  frecfzennn  10863  frecfzen2  10864  seq3val  10897  seqvalcd  10898  seqsplitg  10926  iseqf1olemqcl  10936  iseqf1olemnab  10938  iseqf1olemmo  10942  iseqf1olemqk  10944  seq3f1olemstep  10951  seqf1oglem2  10957  seq3id3  10961  seqhomog  10967  faclbnd  11179  faclbnd3  11181  bcm1k  11198  hashfz1  11222  hashfz  11262  hashfzp1  11265  fiubm  11271  hashfacen  11284  leisorel  11289  wrdexb  11316  wrdsymb  11332  wrdred1hash  11348  lsw0  11352  lswex  11356  ccat0  11364  ccatval2  11366  ccatw2s1leng  11406  ccats1val2  11408  swrds1  11440  swrdlsw  11441  ccats1pfxeqrex  11487  pfxccatin12lem1  11500  swrdccatin2  11501  swrdccat  11507  cats1fvd  11538  s1s2d  11566  s1s3d  11567  cjcj  11648  caucvgre  11747  r19.2uz  11759  resqrexlemgt0  11786  ltabs  11853  xrmaxiflemab  12013  xrmaxiflemlub  12014  nnf1o  12143  summodclem2a  12148  fsumf1o  12157  fisum0diag2  12214  modfsummodlemstep  12224  fsumparts  12237  clim2prod  12306  prodfap0  12312  prodmodclem2a  12343  fprodssdc  12357  fprodcllem  12373  ef0lem  12427  resinval  12482  recosval  12483  demoivreALT  12541  nn0o  12674  gcdmultiplez  12798  dvdssq  12808  nninfct  12818  eucalg  12837  lcmgcdnn  12860  dvdsnprmd  12903  prm2orodd  12904  isprm5lem  12919  qnumdenbi  12970  nn0gcdsq  12978  phibnd  12995  hashdvds  12999  phimullem  13003  prmdiveq  13014  hashgcdlem  13016  modprm0  13033  nnnn0modprm0  13034  modprmn0modprm0  13035  oddprm  13038  prm23lt5  13042  pcprendvds  13069  pcidlem  13102  pcmpt  13122  pcfac  13129  infpnlem2  13139  prmunb  13141  1arith  13146  4sqlem19  13188  ballotfilemfp1  13231  ballotfilemic  13250  ballotfilem1c  13251  ballotfilemsima  13259  ballotfilemrv  13263  ballotfilemro  13266  ballotfilemfrc  13270  ballotfilemfrci  13271  ballotfilemfrceq  13272  ballotfilemfrcn0  13273  ballotfilemrinv0  13276  unennn  13288  ennnfonelemk  13291  ennnfonelemjn  13293  ennnfonelemhf1o  13304  ennnfonelemex  13305  ennnfonelemf1  13309  ennnfonelemrn  13310  qnnen  13322  unbendc  13345  setsfun0  13388  srngbased  13501  srngplusgd  13502  srngmulrd  13503  srnginvld  13504  lmodbased  13519  lmodplusgd  13520  lmodscad  13521  lmodvscad  13522  ipsbased  13531  ipsaddgd  13532  ipsmulrd  13533  ipsscad  13534  ipsvscad  13535  ipsipd  13536  tgval  13616  gzsumval2  13714  isnsgrp  13721  ismnd  13732  dfgrp2e  13833  subgintm  14001  eqg0el  14032  ecqusaddcl  14042  kerf1ghm  14077  gzsumconst  14143  gsumvalfi  14152  gsumf1ofi  14160  prdsbas3  14187  imasrng  14255  srgisid  14290  qusring2  14371  oppr1g  14388  dvdsr02  14412  isunitd  14413  crngunit  14418  unitpropdg  14455  elrhmunit  14484  subrngintm  14520  subrguss  14544  subrgunit  14547  subrgugrp  14548  subrgintm  14551  drngunz  14618  lmodfopnelem1  14661  rmodislmodlem  14687  rmodislmod  14688  lssuni  14700  islss3  14716  lss0v  14767  sraval  14774  rnglidlmmgm  14833  2idllidld  14843  2idlridld  14844  rng2idl0  14856  rng2idlsubg0  14859  zrh0  14960  znle  14972  zndvds0  14985  znf1o  14986  znleval  14988  znfi  14990  znhash  14991  znunit  14994  issubassa  15013  asclfval  15021  ascl0  15027  ascl1  15028  rnasclsubrg  15036  psrbaglecl  15060  psrbasg  15065  psradd  15070  psr0cl  15072  mpladd  15095  cldval  15200  ntrfval  15201  clsfval  15202  neifval  15241  neif  15242  neival  15244  cnclima  15324  cncnpi  15329  cnrest2  15337  cnrest2r  15338  cnptoprest  15340  cnpdis  15343  txvalex  15355  txval  15356  txcnmpt  15374  txdis  15378  cnmpt1t  15386  cnmpt2t  15394  hmeocnv  15408  hmeontr  15414  txhmeo  15420  xmetunirn  15459  xmettpos  15471  metn0  15479  xmetres  15483  metres  15484  blrnps  15512  blrn  15513  blin2  15533  blbas  15534  xmeterval  15536  xmettxlem  15610  xmettx  15611  metcnpi  15616  reldvg  15780  dvaddxx  15804  dvmulxx  15805  dviaddf  15806  dvimulf  15807  dvfre  15811  dvmptid  15817  dveflem  15827  elply2  15836  plyreres  15865  sinq12gt0  15931  logfac  15995  rprelogbdiv  16059  logbgcd1irr  16069  birthdaylem3  16089  fsumdvdsmul  16105  lgslem4  16122  lgsdirprm  16153  gausslemma2dlem0a  16168  gausslemma2dlem0f  16173  gausslemma2dlem0i  16176  gausslemma2dlem1a  16177  gausslemma2dlem1cl  16178  gausslemma2dlem5  16185  gausslemma2dlem6  16186  gausslemma2d  16188  lgseisenlem1  16189  lgseisenlem2  16190  lgseisenlem3  16191  lgseisen  16193  lgsquadlem1  16196  m1lgs  16204  2lgslem1a  16207  2lgslem1c  16209  2lgsoddprmlem2  16225  edgval  16301  edgstruct  16305  umgrnloopv  16355  umgredgprv  16356  upgr1edc  16362  umgredgne  16391  usgredgssen  16403  umgr2edg1  16450  uspgredg2vlem  16461  uspgr1edc  16481  uhgrspansubgrlem  16517  wlkm  16580  wlkvtxiedg  16586  wlkvtxiedgg  16587  wlk1walkdom  16600  g0wlk0  16611  wlkres  16620  trlf1  16629  trlreslem  16630  trlres  16631  clwwlkg  16634  clwwlkccatlem  16641  clwwlknon  16670  eupthfi  16692  eupthseg  16693  eupthres  16698  trlsegvdeglem1  16701  trlsegvdeglem7  16707  trlsegvdegfi  16708  eupth2lem3lem2fi  16710  eupth2lem3lem3fi  16711  eupth2lem3lem6fi  16712  eupth2lem3lem4fi  16714  eupth2lem3lem7fi  16715  eupth2lem3fi  16717  eupth2lemsfi  16719  eupth2fi  16720  konigsbergssiedgwen  16727  bj-inex  16933  bj-sucexg  16948  bj-peano4  16981  setindis  16993  bdsetindis  16995  bj-inf2vnlem1  16996  wexmiddiffilem  17043  wexmiddifxy  17046  nnsf  17048  nninfall  17052  nninfsellemeq  17057  sbthom  17071