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  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  4338  exmid1stab  4343  snelpwi  4349  opth1  4374  frind  4495  onin  4529  abnexg  4590  reusv1  4602  xpexg  4887  reldmm  4998  dmexg  5044  rnexg  5045  elrelimasn  5151  relfld  5314  funimaexglem  5462  funimaexg  5463  fabexg  5577  fsnd  5682  elfvm  5726  nfvres  5729  funimass4  5750  elfvmptrab1  5797  funconstss  5821  f1oresrab  5867  resfunexg  5930  f1eqcocnv  5991  isores1  6014  isoini  6018  isose  6021  isopolem  6022  isosolem  6024  eusvobj2  6065  acexmidlemcase  6074  oprabid  6111  offval  6304  resfunexgALT  6331  offval3  6361  1stvalg  6370  2ndvalg  6371  1stcof  6391  2ndcof  6392  cnvf1o  6455  tposf12  6534  smores3  6558  smoiso  6567  tfr0dm  6587  tfrlemibxssdm  6592  tfrlemi14d  6598  tfrexlem  6599  tfr1onlemssrecs  6604  tfr1onlemsucfn  6605  tfr1onlemsucaccv  6606  tfr1onlembxssdm  6608  tfr1onlemres  6614  tfri1dALT  6616  tfrcllemssrecs  6617  tfrcllemsucfn  6618  tfrcllemsucaccv  6619  tfrcllembxssdm  6621  tfrcllemres  6627  rdgss  6648  nnsucsssuc  6759  nntr2  6770  swoord1  6830  swoord2  6831  iinerm  6875  eroveu  6894  pmresg  6951  en1uniel  7085  dom1o  7110  pw2f1odclem  7128  fopwdom  7130  xpen  7139  mapunen  7145  ssenen  7146  isinfinf  7195  ac6sfi  7196  preimaf1ofi  7262  sbthlem1  7268  fczfsuppd  7291  fi0  7303  fiss  7305  supubti  7333  suplubti  7334  isotilem  7340  supisolem  7342  supisoex  7343  supisoti  7344  ordiso2  7369  eldju1st  7405  eldju2ndl  7406  updjud  7416  djudom  7427  ctmlemr  7442  enumctlemm  7448  nnnninfeq  7462  ctssexmid  7484  nninfwlpoimlemginf  7510  exmidonfinlem  7539  en2other2  7542  exmidaclem  7558  cc2lem  7626  cc3  7628  addclnq  7736  mulclnq  7737  1qec  7749  prarloclemarch2  7780  enq0tr  7795  addclnq0  7812  mulclnq0  7813  nq0m0r  7817  prarloclemlo  7855  prarloc  7864  genpml  7878  genpmu  7879  addnqprl  7890  addnqpru  7891  recnnpr  7909  prmuloc2  7928  1idpru  7952  ltexprlemm  7961  ltexprlemloc  7968  recexprlemm  7985  recexprlem1ssl  7994  caucvgprlemnkj  8027  caucvgprlemnbj  8028  caucvgprlemm  8029  caucvgprlemopl  8030  caucvgprlemlol  8031  caucvgprlemladdfu  8038  caucvgprlemladdrl  8039  caucvgprprlemk  8044  caucvgprprlemloccalc  8045  caucvgprprlemnkltj  8050  caucvgprprlemnjltk  8052  caucvgprprlemml  8055  caucvgprprlemmu  8056  caucvgprprlemlol  8059  caucvgprprlemexb  8068  caucvgprprlem1  8070  suplocexprlemml  8077  suplocexprlemlub  8085  addclsr  8114  mulclsr  8115  prsrcl  8145  caucvgsrlemoffcau  8159  peano5nnnn  8253  mulap0r  8937  nn1suc  9306  prime  9728  zindd  9747  xrlttri3  10182  xnn0xadd0  10252  fzopth  10450  fzsuc  10458  fzpred  10460  fzp1ss  10463  fztp  10468  fseq1p1m1  10484  1fv  10529  elfzom1elp1fzo  10603  ssfzo12  10625  fzosplitsn  10634  zsupcllemstep  10645  zsupcllemex  10646  infssuzledc  10650  divfl0  10714  fldiv4lem1div2uz2  10724  modqid  10769  modqmuladdim  10787  frecuzrdgtcl  10832  frecuzrdgfunlem  10839  frecfzennn  10846  frecfzen2  10847  seq3val  10880  seqvalcd  10881  seqsplitg  10909  iseqf1olemqcl  10919  iseqf1olemnab  10921  iseqf1olemmo  10925  iseqf1olemqk  10927  seq3f1olemstep  10934  seqf1oglem2  10940  seq3id3  10944  seqhomog  10950  faclbnd  11162  faclbnd3  11164  bcm1k  11181  hashfz1  11205  hashfz  11245  hashfzp1  11248  fiubm  11254  hashfacen  11267  leisorel  11272  wrdexb  11299  wrdsymb  11315  wrdred1hash  11331  lsw0  11335  lswex  11339  ccat0  11347  ccatval2  11349  ccatw2s1leng  11389  ccats1val2  11391  swrds1  11423  swrdlsw  11424  ccats1pfxeqrex  11470  pfxccatin12lem1  11483  swrdccatin2  11484  swrdccat  11490  cats1fvd  11521  s1s2d  11549  s1s3d  11550  cjcj  11631  caucvgre  11730  r19.2uz  11742  resqrexlemgt0  11769  ltabs  11836  xrmaxiflemab  11996  xrmaxiflemlub  11997  nnf1o  12126  summodclem2a  12131  fsumf1o  12140  fisum0diag2  12197  modfsummodlemstep  12207  fsumparts  12220  clim2prod  12289  prodfap0  12295  prodmodclem2a  12326  fprodssdc  12340  fprodcllem  12356  ef0lem  12410  resinval  12465  recosval  12466  demoivreALT  12524  nn0o  12657  gcdmultiplez  12781  dvdssq  12791  nninfct  12801  eucalg  12820  lcmgcdnn  12843  dvdsnprmd  12886  prm2orodd  12887  isprm5lem  12902  qnumdenbi  12953  nn0gcdsq  12961  phibnd  12978  hashdvds  12982  phimullem  12986  prmdiveq  12997  hashgcdlem  12999  modprm0  13016  nnnn0modprm0  13017  modprmn0modprm0  13018  oddprm  13021  prm23lt5  13025  pcprendvds  13052  pcidlem  13085  pcmpt  13105  pcfac  13112  infpnlem2  13122  prmunb  13124  1arith  13129  4sqlem19  13171  ballotfilemfp1  13214  ballotfilemic  13233  ballotfilem1c  13234  ballotfilemsima  13242  ballotfilemrv  13246  ballotfilemro  13249  ballotfilemfrc  13253  ballotfilemfrci  13254  ballotfilemfrceq  13255  ballotfilemfrcn0  13256  ballotfilemrinv0  13259  unennn  13271  ennnfonelemk  13274  ennnfonelemjn  13276  ennnfonelemhf1o  13287  ennnfonelemex  13288  ennnfonelemf1  13292  ennnfonelemrn  13293  qnnen  13305  unbendc  13328  setsfun0  13371  srngbased  13484  srngplusgd  13485  srngmulrd  13486  srnginvld  13487  lmodbased  13502  lmodplusgd  13503  lmodscad  13504  lmodvscad  13505  ipsbased  13514  ipsaddgd  13515  ipsmulrd  13516  ipsscad  13517  ipsvscad  13518  ipsipd  13519  tgval  13599  gzsumval2  13697  isnsgrp  13704  ismnd  13715  dfgrp2e  13816  subgintm  13984  eqg0el  14015  ecqusaddcl  14025  kerf1ghm  14060  gzsumconst  14126  gsumvalfi  14135  gsumf1ofi  14143  prdsbas3  14170  imasrng  14238  srgisid  14273  qusring2  14354  oppr1g  14371  dvdsr02  14395  isunitd  14396  crngunit  14401  unitpropdg  14438  elrhmunit  14467  subrngintm  14503  subrguss  14527  subrgunit  14530  subrgugrp  14531  subrgintm  14534  drngunz  14601  lmodfopnelem1  14644  rmodislmodlem  14670  rmodislmod  14671  lssuni  14683  islss3  14699  lss0v  14750  sraval  14757  rnglidlmmgm  14816  2idllidld  14826  2idlridld  14827  rng2idl0  14839  rng2idlsubg0  14842  zrh0  14943  znle  14955  zndvds0  14968  znf1o  14969  znleval  14971  znfi  14973  znhash  14974  znunit  14977  issubassa  14996  asclfval  15004  ascl0  15010  ascl1  15011  rnasclsubrg  15019  psrbaglecl  15043  psrbasg  15048  psradd  15053  psr0cl  15055  mpladd  15078  cldval  15183  ntrfval  15184  clsfval  15185  neifval  15224  neif  15225  neival  15227  cnclima  15307  cncnpi  15312  cnrest2  15320  cnrest2r  15321  cnptoprest  15323  cnpdis  15326  txvalex  15338  txval  15339  txcnmpt  15357  txdis  15361  cnmpt1t  15369  cnmpt2t  15377  hmeocnv  15391  hmeontr  15397  txhmeo  15403  xmetunirn  15442  xmettpos  15454  metn0  15462  xmetres  15466  metres  15467  blrnps  15495  blrn  15496  blin2  15516  blbas  15517  xmeterval  15519  xmettxlem  15593  xmettx  15594  metcnpi  15599  reldvg  15763  dvaddxx  15787  dvmulxx  15788  dviaddf  15789  dvimulf  15790  dvfre  15794  dvmptid  15800  dveflem  15810  elply2  15819  plyreres  15848  sinq12gt0  15914  logfac  15978  rprelogbdiv  16042  logbgcd1irr  16052  birthdaylem3  16072  fsumdvdsmul  16088  lgslem4  16105  lgsdirprm  16136  gausslemma2dlem0a  16151  gausslemma2dlem0f  16156  gausslemma2dlem0i  16159  gausslemma2dlem1a  16160  gausslemma2dlem1cl  16161  gausslemma2dlem5  16168  gausslemma2dlem6  16169  gausslemma2d  16171  lgseisenlem1  16172  lgseisenlem2  16173  lgseisenlem3  16174  lgseisen  16176  lgsquadlem1  16179  m1lgs  16187  2lgslem1a  16190  2lgslem1c  16192  2lgsoddprmlem2  16208  edgval  16284  edgstruct  16288  umgrnloopv  16338  umgredgprv  16339  upgr1edc  16345  umgredgne  16374  usgredgssen  16386  umgr2edg1  16433  uspgredg2vlem  16444  uspgr1edc  16464  uhgrspansubgrlem  16500  wlkm  16563  wlkvtxiedg  16569  wlkvtxiedgg  16570  wlk1walkdom  16583  g0wlk0  16594  wlkres  16603  trlf1  16612  trlreslem  16613  trlres  16614  clwwlkg  16617  clwwlkccatlem  16624  clwwlknon  16653  eupthfi  16675  eupthseg  16676  eupthres  16681  trlsegvdeglem1  16684  trlsegvdeglem7  16690  trlsegvdegfi  16691  eupth2lem3lem2fi  16693  eupth2lem3lem3fi  16694  eupth2lem3lem6fi  16695  eupth2lem3lem4fi  16697  eupth2lem3lem7fi  16698  eupth2lem3fi  16700  eupth2lemsfi  16702  eupth2fi  16703  konigsbergssiedgwen  16710  bj-inex  16916  bj-sucexg  16931  bj-peano4  16964  setindis  16976  bdsetindis  16978  bj-inf2vnlem1  16979  nnsf  17022  nninfall  17026  nninfsellemeq  17031  sbthom  17045