Theorem 3syl 17

Description: Inference chaining two syllogisms. (Contributed by NM, 5-Aug-1993.)

Hypotheses

Ref	Expression
3syl.1	⊢ (𝜑 → 𝜓)
3syl.2	⊢ (𝜓 → 𝜒)
3syl.3	⊢ (𝜒 → 𝜃)

Assertion

Ref	Expression
3syl	⊢ (𝜑 → 𝜃)

Proof of Theorem 3syl

Step	Hyp	Ref	Expression
1		3syl.1	. . 3 ⊢ (𝜑 → 𝜓)
2		3syl.2	. . 3 ⊢ (𝜓 → 𝜒)
3	1, 2	syl 14	. 2 ⊢ (𝜑 → 𝜒)
4		3syl.3	. 2 ⊢ (𝜒 → 𝜃)
5	3, 4	syl 14	1 ⊢ (𝜑 → 𝜃)

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  1591  nfal  1622  19.9hd  1708  equsexd  1775  sbcof2  1856  aev  1858  sbequi  1885  nfsbd  2028  mo2n  2105  eupickb  2159  r19.29af2  2671  spc2gv  2894  spc3gv  2896  eqvincg  2927  sbcco3g  3182  ssrmof  3287  exmidsssnc  4286  exmid1stab  4291  snelpwi  4296  opth1  4321  frind  4440  onin  4474  abnexg  4534  reusv1  4546  xpexg  4830  dmexg  4984  rnexg  4985  elrelimasn  5090  relfld  5253  funimaexglem  5400  funimaexg  5401  fabexg  5509  fsnd  5612  elfvm  5656  nfvres  5657  funimass4  5677  elfvmptrab1  5722  funconstss  5746  f1oresrab  5793  resfunexg  5853  f1eqcocnv  5908  isores1  5931  isoini  5935  isose  5938  isopolem  5939  isosolem  5941  eusvobj2  5980  acexmidlemcase  5989  oprabid  6026  offval  6216  resfunexgALT  6243  offval3  6269  1stvalg  6278  2ndvalg  6279  1stcof  6299  2ndcof  6300  cnvf1o  6361  tposf12  6405  smores3  6429  smoiso  6438  tfr0dm  6458  tfrlemibxssdm  6463  tfrlemi14d  6469  tfrexlem  6470  tfr1onlemssrecs  6475  tfr1onlemsucfn  6476  tfr1onlemsucaccv  6477  tfr1onlembxssdm  6479  tfr1onlemres  6485  tfri1dALT  6487  tfrcllemssrecs  6488  tfrcllemsucfn  6489  tfrcllemsucaccv  6490  tfrcllembxssdm  6492  tfrcllemres  6498  rdgss  6519  nnsucsssuc  6628  nntr2  6639  swoord1  6699  swoord2  6700  iinerm  6744  eroveu  6763  pmresg  6813  en1uniel  6946  pw2f1odclem  6983  fopwdom  6985  xpen  6994  ssenen  7000  isinfinf  7047  ac6sfi  7048  preimaf1ofi  7106  sbthlem1  7112  fi0  7130  fiss  7132  supubti  7154  suplubti  7155  isotilem  7161  supisolem  7163  supisoex  7164  supisoti  7165  ordiso2  7190  eldju1st  7226  eldju2ndl  7227  updjud  7237  djudom  7248  ctmlemr  7263  enumctlemm  7269  nnnninfeq  7283  ctssexmid  7305  nninfwlpoimlemginf  7331  exmidonfinlem  7359  en2other2  7362  exmidaclem  7378  cc2lem  7440  cc3  7442  addclnq  7550  mulclnq  7551  1qec  7563  prarloclemarch2  7594  enq0tr  7609  addclnq0  7626  mulclnq0  7627  nq0m0r  7631  prarloclemlo  7669  prarloc  7678  genpml  7692  genpmu  7693  addnqprl  7704  addnqpru  7705  recnnpr  7723  prmuloc2  7742  1idpru  7766  ltexprlemm  7775  ltexprlemloc  7782  recexprlemm  7799  recexprlem1ssl  7808  caucvgprlemnkj  7841  caucvgprlemnbj  7842  caucvgprlemm  7843  caucvgprlemopl  7844  caucvgprlemlol  7845  caucvgprlemladdfu  7852  caucvgprlemladdrl  7853  caucvgprprlemk  7858  caucvgprprlemloccalc  7859  caucvgprprlemnkltj  7864  caucvgprprlemnjltk  7866  caucvgprprlemml  7869  caucvgprprlemmu  7870  caucvgprprlemlol  7873  caucvgprprlemexb  7882  caucvgprprlem1  7884  suplocexprlemml  7891  suplocexprlemlub  7899  addclsr  7928  mulclsr  7929  prsrcl  7959  caucvgsrlemoffcau  7973  peano5nnnn  8067  mulap0r  8750  nn1suc  9117  prime  9534  zindd  9553  xrlttri3  9981  xnn0xadd0  10051  fzopth  10245  fzsuc  10253  fzpred  10254  fzp1ss  10257  fztp  10262  fseq1p1m1  10278  1fv  10323  elfzom1elp1fzo  10395  ssfzo12  10417  fzosplitsn  10426  zsupcllemstep  10436  zsupcllemex  10437  infssuzledc  10441  divfl0  10503  fldiv4lem1div2uz2  10513  modqid  10558  modqmuladdim  10576  frecuzrdgtcl  10621  frecuzrdgfunlem  10628  frecfzennn  10635  frecfzen2  10636  seq3val  10669  seqvalcd  10670  seqsplitg  10698  iseqf1olemqcl  10708  iseqf1olemnab  10710  iseqf1olemmo  10714  iseqf1olemqk  10716  seq3f1olemstep  10723  seqf1oglem2  10729  seq3id3  10733  seqhomog  10739  faclbnd  10950  faclbnd3  10952  bcm1k  10969  hashfz1  10992  hashfz  11030  hashfzp1  11033  fiubm  11037  hashfacen  11045  leisorel  11046  wrdexb  11070  wrdsymb  11085  wrdred1hash  11101  lsw0  11105  lswex  11109  ccat0  11117  ccatval2  11119  ccats1val2  11157  swrds1  11186  swrdlsw  11187  ccats1pfxeqrex  11233  pfxccatin12lem1  11246  swrdccatin2  11247  swrdccat  11253  cats1fvd  11284  cjcj  11380  caucvgre  11478  r19.2uz  11490  resqrexlemgt0  11517  ltabs  11584  xrmaxiflemab  11744  xrmaxiflemlub  11745  nnf1o  11873  summodclem2a  11878  fsumf1o  11887  fisum0diag2  11944  modfsummodlemstep  11954  fsumparts  11967  clim2prod  12036  prodfap0  12042  prodmodclem2a  12073  fprodssdc  12087  fprodcllem  12103  ef0lem  12157  resinval  12212  recosval  12213  demoivreALT  12271  nn0o  12404  gcdmultiplez  12528  dvdssq  12538  nninfct  12548  eucalg  12567  lcmgcdnn  12590  dvdsnprmd  12633  prm2orodd  12634  isprm5lem  12649  qnumdenbi  12700  nn0gcdsq  12708  phibnd  12725  hashdvds  12729  phimullem  12733  prmdiveq  12744  hashgcdlem  12746  modprm0  12763  nnnn0modprm0  12764  modprmn0modprm0  12765  oddprm  12768  prm23lt5  12772  pcprendvds  12799  pcidlem  12832  pcmpt  12852  pcfac  12859  infpnlem2  12869  prmunb  12871  1arith  12876  4sqlem19  12918  unennn  12954  ennnfonelemk  12957  ennnfonelemjn  12959  ennnfonelemhf1o  12970  ennnfonelemex  12971  ennnfonelemf1  12975  ennnfonelemrn  12976  qnnen  12988  unbendc  13011  setsfun0  13054  srngbased  13166  srngplusgd  13167  srngmulrd  13168  srnginvld  13169  lmodbased  13184  lmodplusgd  13185  lmodscad  13186  lmodvscad  13187  ipsbased  13196  ipsaddgd  13197  ipsmulrd  13198  ipsscad  13199  ipsvscad  13200  ipsipd  13201  tgval  13281  prdsbas3  13306  isnsgrp  13425  ismnd  13438  dfgrp2e  13547  subgintm  13721  eqg0el  13752  ecqusaddcl  13762  kerf1ghm  13797  gsumfzconst  13864  imasrng  13905  srgisid  13935  srg1zr  13936  qusring2  14015  oppr1g  14031  dvdsr02  14054  isunitd  14055  crngunit  14060  unitpropdg  14097  elrhmunit  14126  subrngintm  14161  subrguss  14185  subrgunit  14188  subrgugrp  14189  subrgintm  14192  lmodfopnelem1  14273  rmodislmodlem  14299  rmodislmod  14300  lssuni  14312  islss3  14328  lss0v  14379  sraval  14386  rnglidlmmgm  14445  2idllidld  14455  2idlridld  14456  rng2idl0  14468  rng2idlsubg0  14471  zrh0  14574  znle  14586  zndvds0  14599  znf1o  14600  znleval  14602  znfi  14604  znhash  14605  znunit  14608  psrbasg  14623  psradd  14628  psr0cl  14630  mpladd  14653  cldval  14758  ntrfval  14759  clsfval  14760  neifval  14799  neif  14800  neival  14802  cnclima  14882  cncnpi  14887  cnrest2  14895  cnrest2r  14896  cnptoprest  14898  cnpdis  14901  txvalex  14913  txval  14914  txcnmpt  14932  txdis  14936  cnmpt1t  14944  cnmpt2t  14952  hmeocnv  14966  hmeontr  14972  txhmeo  14978  xmetunirn  15017  xmettpos  15029  metn0  15037  xmetres  15041  metres  15042  blrnps  15070  blrn  15071  blin2  15091  blbas  15092  xmeterval  15094  xmettxlem  15168  xmettx  15169  metcnpi  15174  reldvg  15338  dvaddxx  15362  dvmulxx  15363  dviaddf  15364  dvimulf  15365  dvfre  15369  dvmptid  15375  dveflem  15385  elply2  15394  plyreres  15423  sinq12gt0  15489  rprelogbdiv  15616  logbgcd1irr  15626  fsumdvdsmul  15650  lgslem4  15667  lgsdirprm  15698  gausslemma2dlem0a  15713  gausslemma2dlem0f  15718  gausslemma2dlem0i  15721  gausslemma2dlem1a  15722  gausslemma2dlem1cl  15723  gausslemma2dlem5  15730  gausslemma2dlem6  15731  gausslemma2d  15733  lgseisenlem1  15734  lgseisenlem2  15735  lgseisenlem3  15736  lgseisen  15738  lgsquadlem1  15741  m1lgs  15749  2lgslem1a  15752  2lgslem1c  15754  2lgsoddprmlem2  15770  edgstruct  15849  umgrnloopv  15899  umgredgprv  15900  upgr1edc  15906  umgredgne  15933  usgredgssen  15945  umgr2edg1  15992  uspgredg2vlem  16003  bj-inex  16200  bj-sucexg  16215  bj-peano4  16248  setindis  16260  bdsetindis  16262  bj-inf2vnlem1  16263  dom1o  16286  nnsf  16302  nninfall  16306  nninfsellemeq  16311  sbthom  16325