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  1594  nfal  1625  19.9hd  1710  equsexd  1778  sbcof2  1859  aev  1861  sbequi  1888  nfsbd  2033  mo2n  2110  eupickb  2164  r19.29af2  2685  spc2gv  2910  spc3gv  2912  eqvincg  2944  sbcco3g  3199  ssrmof  3305  exmidsssnc  4321  exmid1stab  4326  snelpwi  4332  opth1  4357  frind  4478  onin  4512  abnexg  4572  reusv1  4584  xpexg  4869  reldmm  4980  dmexg  5026  rnexg  5027  elrelimasn  5133  relfld  5296  funimaexglem  5444  funimaexg  5445  fabexg  5559  fsnd  5664  elfvm  5708  nfvres  5711  funimass4  5732  elfvmptrab1  5777  funconstss  5801  f1oresrab  5847  resfunexg  5910  f1eqcocnv  5970  isores1  5993  isoini  5997  isose  6000  isopolem  6001  isosolem  6003  eusvobj2  6044  acexmidlemcase  6053  oprabid  6090  offval  6283  resfunexgALT  6310  offval3  6340  1stvalg  6349  2ndvalg  6350  1stcof  6370  2ndcof  6371  cnvf1o  6434  tposf12  6513  smores3  6537  smoiso  6546  tfr0dm  6566  tfrlemibxssdm  6571  tfrlemi14d  6577  tfrexlem  6578  tfr1onlemssrecs  6583  tfr1onlemsucfn  6584  tfr1onlemsucaccv  6585  tfr1onlembxssdm  6587  tfr1onlemres  6593  tfri1dALT  6595  tfrcllemssrecs  6596  tfrcllemsucfn  6597  tfrcllemsucaccv  6598  tfrcllembxssdm  6600  tfrcllemres  6606  rdgss  6627  nnsucsssuc  6738  nntr2  6749  swoord1  6809  swoord2  6810  iinerm  6854  eroveu  6873  pmresg  6923  en1uniel  7057  dom1o  7082  pw2f1odclem  7100  fopwdom  7102  xpen  7111  mapunen  7117  ssenen  7118  isinfinf  7167  ac6sfi  7168  preimaf1ofi  7234  sbthlem1  7240  fczfsuppd  7263  fi0  7275  fiss  7277  supubti  7303  suplubti  7304  isotilem  7310  supisolem  7312  supisoex  7313  supisoti  7314  ordiso2  7339  eldju1st  7375  eldju2ndl  7376  updjud  7386  djudom  7397  ctmlemr  7412  enumctlemm  7418  nnnninfeq  7432  ctssexmid  7454  nninfwlpoimlemginf  7480  exmidonfinlem  7509  en2other2  7512  exmidaclem  7528  cc2lem  7596  cc3  7598  addclnq  7706  mulclnq  7707  1qec  7719  prarloclemarch2  7750  enq0tr  7765  addclnq0  7782  mulclnq0  7783  nq0m0r  7787  prarloclemlo  7825  prarloc  7834  genpml  7848  genpmu  7849  addnqprl  7860  addnqpru  7861  recnnpr  7879  prmuloc2  7898  1idpru  7922  ltexprlemm  7931  ltexprlemloc  7938  recexprlemm  7955  recexprlem1ssl  7964  caucvgprlemnkj  7997  caucvgprlemnbj  7998  caucvgprlemm  7999  caucvgprlemopl  8000  caucvgprlemlol  8001  caucvgprlemladdfu  8008  caucvgprlemladdrl  8009  caucvgprprlemk  8014  caucvgprprlemloccalc  8015  caucvgprprlemnkltj  8020  caucvgprprlemnjltk  8022  caucvgprprlemml  8025  caucvgprprlemmu  8026  caucvgprprlemlol  8029  caucvgprprlemexb  8038  caucvgprprlem1  8040  suplocexprlemml  8047  suplocexprlemlub  8055  addclsr  8084  mulclsr  8085  prsrcl  8115  caucvgsrlemoffcau  8129  peano5nnnn  8223  mulap0r  8907  nn1suc  9276  prime  9698  zindd  9717  xrlttri3  10152  xnn0xadd0  10222  fzopth  10419  fzsuc  10427  fzpred  10429  fzp1ss  10432  fztp  10437  fseq1p1m1  10453  1fv  10498  elfzom1elp1fzo  10572  ssfzo12  10594  fzosplitsn  10603  zsupcllemstep  10614  zsupcllemex  10615  infssuzledc  10619  divfl0  10683  fldiv4lem1div2uz2  10693  modqid  10738  modqmuladdim  10756  frecuzrdgtcl  10801  frecuzrdgfunlem  10808  frecfzennn  10815  frecfzen2  10816  seq3val  10849  seqvalcd  10850  seqsplitg  10878  iseqf1olemqcl  10888  iseqf1olemnab  10890  iseqf1olemmo  10894  iseqf1olemqk  10896  seq3f1olemstep  10903  seqf1oglem2  10909  seq3id3  10913  seqhomog  10919  faclbnd  11131  faclbnd3  11133  bcm1k  11150  hashfz1  11174  hashfz  11214  hashfzp1  11217  fiubm  11223  hashfacen  11236  leisorel  11237  wrdexb  11264  wrdsymb  11280  wrdred1hash  11296  lsw0  11300  lswex  11304  ccat0  11312  ccatval2  11314  ccatw2s1leng  11354  ccats1val2  11356  swrds1  11388  swrdlsw  11389  ccats1pfxeqrex  11435  pfxccatin12lem1  11448  swrdccatin2  11449  swrdccat  11455  cats1fvd  11486  s1s2d  11514  s1s3d  11515  cjcj  11596  caucvgre  11695  r19.2uz  11707  resqrexlemgt0  11734  ltabs  11801  xrmaxiflemab  11961  xrmaxiflemlub  11962  nnf1o  12091  summodclem2a  12096  fsumf1o  12105  fisum0diag2  12162  modfsummodlemstep  12172  fsumparts  12185  clim2prod  12254  prodfap0  12260  prodmodclem2a  12291  fprodssdc  12305  fprodcllem  12321  ef0lem  12375  resinval  12430  recosval  12431  demoivreALT  12489  nn0o  12622  gcdmultiplez  12746  dvdssq  12756  nninfct  12766  eucalg  12785  lcmgcdnn  12808  dvdsnprmd  12851  prm2orodd  12852  isprm5lem  12867  qnumdenbi  12918  nn0gcdsq  12926  phibnd  12943  hashdvds  12947  phimullem  12951  prmdiveq  12962  hashgcdlem  12964  modprm0  12981  nnnn0modprm0  12982  modprmn0modprm0  12983  oddprm  12986  prm23lt5  12990  pcprendvds  13017  pcidlem  13050  pcmpt  13070  pcfac  13077  infpnlem2  13087  prmunb  13089  1arith  13094  4sqlem19  13136  ballotfilemfp1  13179  ballotfilemic  13198  ballotfilem1c  13199  ballotfilemsima  13207  ballotfilemrv  13211  ballotfilemro  13214  ballotfilemfrc  13218  ballotfilemfrci  13219  ballotfilemfrceq  13220  ballotfilemfrcn0  13221  ballotfilemrinv0  13224  unennn  13236  ennnfonelemk  13239  ennnfonelemjn  13241  ennnfonelemhf1o  13252  ennnfonelemex  13253  ennnfonelemf1  13257  ennnfonelemrn  13258  qnnen  13270  unbendc  13293  setsfun0  13336  srngbased  13448  srngplusgd  13449  srngmulrd  13450  srnginvld  13451  lmodbased  13466  lmodplusgd  13467  lmodscad  13468  lmodvscad  13469  ipsbased  13478  ipsaddgd  13479  ipsmulrd  13480  ipsscad  13481  ipsvscad  13482  ipsipd  13483  tgval  13563  isnsgrp  13673  ismnd  13684  dfgrp2e  13787  subgintm  13955  eqg0el  13986  ecqusaddcl  13996  kerf1ghm  14031  gsumfzconst  14098  gfsumval  14106  prdsbas3  14133  imasrng  14199  srgisid  14233  qusring2  14313  oppr1g  14330  dvdsr02  14354  isunitd  14355  crngunit  14360  unitpropdg  14397  elrhmunit  14426  subrngintm  14462  subrguss  14486  subrgunit  14489  subrgugrp  14490  subrgintm  14493  drngunz  14560  lmodfopnelem1  14602  rmodislmodlem  14628  rmodislmod  14629  lssuni  14641  islss3  14657  lss0v  14708  sraval  14715  rnglidlmmgm  14774  2idllidld  14784  2idlridld  14785  rng2idl0  14797  rng2idlsubg0  14800  zrh0  14903  znle  14915  zndvds0  14928  znf1o  14929  znleval  14931  znfi  14933  znhash  14934  znunit  14937  psrbaglecl  14954  psrbasg  14959  psradd  14964  psr0cl  14966  mpladd  14989  cldval  15094  ntrfval  15095  clsfval  15096  neifval  15135  neif  15136  neival  15138  cnclima  15218  cncnpi  15223  cnrest2  15231  cnrest2r  15232  cnptoprest  15234  cnpdis  15237  txvalex  15249  txval  15250  txcnmpt  15268  txdis  15272  cnmpt1t  15280  cnmpt2t  15288  hmeocnv  15302  hmeontr  15308  txhmeo  15314  xmetunirn  15353  xmettpos  15365  metn0  15373  xmetres  15377  metres  15378  blrnps  15406  blrn  15407  blin2  15427  blbas  15428  xmeterval  15430  xmettxlem  15504  xmettx  15505  metcnpi  15510  reldvg  15674  dvaddxx  15698  dvmulxx  15699  dviaddf  15700  dvimulf  15701  dvfre  15705  dvmptid  15711  dveflem  15721  elply2  15730  plyreres  15759  sinq12gt0  15825  rprelogbdiv  15952  logbgcd1irr  15962  fsumdvdsmul  15989  lgslem4  16006  lgsdirprm  16037  gausslemma2dlem0a  16052  gausslemma2dlem0f  16057  gausslemma2dlem0i  16060  gausslemma2dlem1a  16061  gausslemma2dlem1cl  16062  gausslemma2dlem5  16069  gausslemma2dlem6  16070  gausslemma2d  16072  lgseisenlem1  16073  lgseisenlem2  16074  lgseisenlem3  16075  lgseisen  16077  lgsquadlem1  16080  m1lgs  16088  2lgslem1a  16091  2lgslem1c  16093  2lgsoddprmlem2  16109  edgval  16185  edgstruct  16189  umgrnloopv  16239  umgredgprv  16240  upgr1edc  16246  umgredgne  16275  usgredgssen  16287  umgr2edg1  16334  uspgredg2vlem  16345  uspgr1edc  16365  uhgrspansubgrlem  16401  wlkm  16464  wlkvtxiedg  16470  wlkvtxiedgg  16471  wlk1walkdom  16484  g0wlk0  16495  wlkres  16504  trlf1  16513  trlreslem  16514  trlres  16515  clwwlkg  16518  clwwlkccatlem  16525  clwwlknon  16554  eupthfi  16576  eupthseg  16577  eupthres  16582  trlsegvdeglem1  16585  trlsegvdeglem7  16591  trlsegvdegfi  16592  eupth2lem3lem2fi  16594  eupth2lem3lem3fi  16595  eupth2lem3lem6fi  16596  eupth2lem3lem4fi  16598  eupth2lem3lem7fi  16599  eupth2lem3fi  16601  eupth2lemsfi  16603  eupth2fi  16604  konigsbergssiedgwen  16611  bj-inex  16817  bj-sucexg  16832  bj-peano4  16865  setindis  16877  bdsetindis  16879  bj-inf2vnlem1  16880  nnsf  16923  nninfall  16927  nninfsellemeq  16932  sbthom  16946