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  8906  nn1suc  9273  prime  9695  zindd  9714  xrlttri3  10149  xnn0xadd0  10219  fzopth  10416  fzsuc  10424  fzpred  10426  fzp1ss  10429  fztp  10434  fseq1p1m1  10450  1fv  10495  elfzom1elp1fzo  10569  ssfzo12  10591  fzosplitsn  10600  zsupcllemstep  10611  zsupcllemex  10612  infssuzledc  10616  divfl0  10680  fldiv4lem1div2uz2  10690  modqid  10735  modqmuladdim  10753  frecuzrdgtcl  10798  frecuzrdgfunlem  10805  frecfzennn  10812  frecfzen2  10813  seq3val  10846  seqvalcd  10847  seqsplitg  10875  iseqf1olemqcl  10885  iseqf1olemnab  10887  iseqf1olemmo  10891  iseqf1olemqk  10893  seq3f1olemstep  10900  seqf1oglem2  10906  seq3id3  10910  seqhomog  10916  faclbnd  11128  faclbnd3  11130  bcm1k  11147  hashfz1  11171  hashfz  11211  hashfzp1  11214  fiubm  11220  hashfacen  11233  leisorel  11234  wrdexb  11261  wrdsymb  11277  wrdred1hash  11293  lsw0  11297  lswex  11301  ccat0  11309  ccatval2  11311  ccatw2s1leng  11351  ccats1val2  11353  swrds1  11385  swrdlsw  11386  ccats1pfxeqrex  11432  pfxccatin12lem1  11445  swrdccatin2  11446  swrdccat  11452  cats1fvd  11483  s1s2d  11511  s1s3d  11512  cjcj  11593  caucvgre  11691  r19.2uz  11703  resqrexlemgt0  11730  ltabs  11797  xrmaxiflemab  11957  xrmaxiflemlub  11958  nnf1o  12087  summodclem2a  12092  fsumf1o  12101  fisum0diag2  12158  modfsummodlemstep  12168  fsumparts  12181  clim2prod  12250  prodfap0  12256  prodmodclem2a  12287  fprodssdc  12301  fprodcllem  12317  ef0lem  12371  resinval  12426  recosval  12427  demoivreALT  12485  nn0o  12618  gcdmultiplez  12742  dvdssq  12752  nninfct  12762  eucalg  12781  lcmgcdnn  12804  dvdsnprmd  12847  prm2orodd  12848  isprm5lem  12863  qnumdenbi  12914  nn0gcdsq  12922  phibnd  12939  hashdvds  12943  phimullem  12947  prmdiveq  12958  hashgcdlem  12960  modprm0  12977  nnnn0modprm0  12978  modprmn0modprm0  12979  oddprm  12982  prm23lt5  12986  pcprendvds  13013  pcidlem  13046  pcmpt  13066  pcfac  13073  infpnlem2  13083  prmunb  13085  1arith  13090  4sqlem19  13132  ballotfilemfp1  13175  ballotfilemic  13194  ballotfilem1c  13195  ballotfilemsima  13203  ballotfilemrv  13207  ballotfilemro  13210  ballotfilemfrc  13214  ballotfilemfrci  13215  ballotfilemfrceq  13216  ballotfilemfrcn0  13217  ballotfilemrinv0  13220  unennn  13232  ennnfonelemk  13235  ennnfonelemjn  13237  ennnfonelemhf1o  13248  ennnfonelemex  13249  ennnfonelemf1  13253  ennnfonelemrn  13254  qnnen  13266  unbendc  13289  setsfun0  13332  srngbased  13444  srngplusgd  13445  srngmulrd  13446  srnginvld  13447  lmodbased  13462  lmodplusgd  13463  lmodscad  13464  lmodvscad  13465  ipsbased  13474  ipsaddgd  13475  ipsmulrd  13476  ipsscad  13477  ipsvscad  13478  ipsipd  13479  tgval  13559  prdsbas3  13584  isnsgrp  13703  ismnd  13716  dfgrp2e  13825  subgintm  13999  eqg0el  14030  ecqusaddcl  14040  kerf1ghm  14075  gsumfzconst  14142  imasrng  14184  srgisid  14214  srg1zr  14215  qusring2  14294  oppr1g  14311  dvdsr02  14335  isunitd  14336  crngunit  14341  unitpropdg  14378  elrhmunit  14407  subrngintm  14443  subrguss  14467  subrgunit  14470  subrgugrp  14471  subrgintm  14474  drngunz  14541  lmodfopnelem1  14584  rmodislmodlem  14610  rmodislmod  14611  lssuni  14623  islss3  14639  lss0v  14690  sraval  14697  rnglidlmmgm  14756  2idllidld  14766  2idlridld  14767  rng2idl0  14779  rng2idlsubg0  14782  zrh0  14885  znle  14897  zndvds0  14910  znf1o  14911  znleval  14913  znfi  14915  znhash  14916  znunit  14919  psrbaglecl  14936  psrbasg  14941  psradd  14946  psr0cl  14948  mpladd  14971  cldval  15076  ntrfval  15077  clsfval  15078  neifval  15117  neif  15118  neival  15120  cnclima  15200  cncnpi  15205  cnrest2  15213  cnrest2r  15214  cnptoprest  15216  cnpdis  15219  txvalex  15231  txval  15232  txcnmpt  15250  txdis  15254  cnmpt1t  15262  cnmpt2t  15270  hmeocnv  15284  hmeontr  15290  txhmeo  15296  xmetunirn  15335  xmettpos  15347  metn0  15355  xmetres  15359  metres  15360  blrnps  15388  blrn  15389  blin2  15409  blbas  15410  xmeterval  15412  xmettxlem  15486  xmettx  15487  metcnpi  15492  reldvg  15656  dvaddxx  15680  dvmulxx  15681  dviaddf  15682  dvimulf  15683  dvfre  15687  dvmptid  15693  dveflem  15703  elply2  15712  plyreres  15741  sinq12gt0  15807  rprelogbdiv  15934  logbgcd1irr  15944  fsumdvdsmul  15971  lgslem4  15988  lgsdirprm  16019  gausslemma2dlem0a  16034  gausslemma2dlem0f  16039  gausslemma2dlem0i  16042  gausslemma2dlem1a  16043  gausslemma2dlem1cl  16044  gausslemma2dlem5  16051  gausslemma2dlem6  16052  gausslemma2d  16054  lgseisenlem1  16055  lgseisenlem2  16056  lgseisenlem3  16057  lgseisen  16059  lgsquadlem1  16062  m1lgs  16070  2lgslem1a  16073  2lgslem1c  16075  2lgsoddprmlem2  16091  edgval  16167  edgstruct  16171  umgrnloopv  16221  umgredgprv  16222  upgr1edc  16228  umgredgne  16257  usgredgssen  16269  umgr2edg1  16316  uspgredg2vlem  16327  uspgr1edc  16347  uhgrspansubgrlem  16383  wlkm  16446  wlkvtxiedg  16452  wlkvtxiedgg  16453  wlk1walkdom  16466  g0wlk0  16477  wlkres  16486  trlf1  16495  trlreslem  16496  trlres  16497  clwwlkg  16500  clwwlkccatlem  16507  clwwlknon  16536  eupthfi  16558  eupthseg  16559  eupthres  16564  trlsegvdeglem1  16567  trlsegvdeglem7  16573  trlsegvdegfi  16574  eupth2lem3lem2fi  16576  eupth2lem3lem3fi  16577  eupth2lem3lem6fi  16578  eupth2lem3lem4fi  16580  eupth2lem3lem7fi  16581  eupth2lem3fi  16583  eupth2lemsfi  16585  eupth2fi  16586  konigsbergssiedgwen  16593  bj-inex  16789  bj-sucexg  16804  bj-peano4  16837  setindis  16849  bdsetindis  16851  bj-inf2vnlem1  16852  nnsf  16895  nninfall  16899  nninfsellemeq  16904  sbthom  16918  gfsumval  16974