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  2031  mo2n  2108  eupickb  2162  r19.29af2  2683  spc2gv  2907  spc3gv  2909  eqvincg  2940  sbcco3g  3195  ssrmof  3300  exmidsssnc  4315  exmid1stab  4320  snelpwi  4326  opth1  4351  frind  4472  onin  4506  abnexg  4566  reusv1  4578  xpexg  4863  reldmm  4974  dmexg  5020  rnexg  5021  elrelimasn  5127  relfld  5290  funimaexglem  5438  funimaexg  5439  fabexg  5553  fsnd  5658  elfvm  5702  nfvres  5705  funimass4  5726  elfvmptrab1  5771  funconstss  5795  f1oresrab  5841  resfunexg  5904  f1eqcocnv  5963  isores1  5986  isoini  5990  isose  5993  isopolem  5994  isosolem  5996  eusvobj2  6035  acexmidlemcase  6044  oprabid  6081  offval  6273  resfunexgALT  6300  offval3  6326  1stvalg  6335  2ndvalg  6336  1stcof  6356  2ndcof  6357  cnvf1o  6420  tposf12  6499  smores3  6523  smoiso  6532  tfr0dm  6552  tfrlemibxssdm  6557  tfrlemi14d  6563  tfrexlem  6564  tfr1onlemssrecs  6569  tfr1onlemsucfn  6570  tfr1onlemsucaccv  6571  tfr1onlembxssdm  6573  tfr1onlemres  6579  tfri1dALT  6581  tfrcllemssrecs  6582  tfrcllemsucfn  6583  tfrcllemsucaccv  6584  tfrcllembxssdm  6586  tfrcllemres  6592  rdgss  6613  nnsucsssuc  6724  nntr2  6735  swoord1  6795  swoord2  6796  iinerm  6840  eroveu  6859  pmresg  6909  en1uniel  7043  dom1o  7068  pw2f1odclem  7086  fopwdom  7088  xpen  7097  mapunen  7103  ssenen  7104  isinfinf  7153  ac6sfi  7154  preimaf1ofi  7220  sbthlem1  7226  fczfsuppd  7249  fi0  7261  fiss  7263  supubti  7289  suplubti  7290  isotilem  7296  supisolem  7298  supisoex  7299  supisoti  7300  ordiso2  7325  eldju1st  7361  eldju2ndl  7362  updjud  7372  djudom  7383  ctmlemr  7398  enumctlemm  7404  nnnninfeq  7418  ctssexmid  7440  nninfwlpoimlemginf  7466  exmidonfinlem  7495  en2other2  7498  exmidaclem  7514  cc2lem  7579  cc3  7581  addclnq  7689  mulclnq  7690  1qec  7702  prarloclemarch2  7733  enq0tr  7748  addclnq0  7765  mulclnq0  7766  nq0m0r  7770  prarloclemlo  7808  prarloc  7817  genpml  7831  genpmu  7832  addnqprl  7843  addnqpru  7844  recnnpr  7862  prmuloc2  7881  1idpru  7905  ltexprlemm  7914  ltexprlemloc  7921  recexprlemm  7938  recexprlem1ssl  7947  caucvgprlemnkj  7980  caucvgprlemnbj  7981  caucvgprlemm  7982  caucvgprlemopl  7983  caucvgprlemlol  7984  caucvgprlemladdfu  7991  caucvgprlemladdrl  7992  caucvgprprlemk  7997  caucvgprprlemloccalc  7998  caucvgprprlemnkltj  8003  caucvgprprlemnjltk  8005  caucvgprprlemml  8008  caucvgprprlemmu  8009  caucvgprprlemlol  8012  caucvgprprlemexb  8021  caucvgprprlem1  8023  suplocexprlemml  8030  suplocexprlemlub  8038  addclsr  8067  mulclsr  8068  prsrcl  8098  caucvgsrlemoffcau  8112  peano5nnnn  8206  mulap0r  8888  nn1suc  9255  prime  9676  zindd  9695  xrlttri3  10129  xnn0xadd0  10199  fzopth  10394  fzsuc  10402  fzpred  10403  fzp1ss  10406  fztp  10411  fseq1p1m1  10427  1fv  10472  elfzom1elp1fzo  10546  ssfzo12  10568  fzosplitsn  10577  zsupcllemstep  10588  zsupcllemex  10589  infssuzledc  10593  divfl0  10655  fldiv4lem1div2uz2  10665  modqid  10710  modqmuladdim  10728  frecuzrdgtcl  10773  frecuzrdgfunlem  10780  frecfzennn  10787  frecfzen2  10788  seq3val  10821  seqvalcd  10822  seqsplitg  10850  iseqf1olemqcl  10860  iseqf1olemnab  10862  iseqf1olemmo  10866  iseqf1olemqk  10868  seq3f1olemstep  10875  seqf1oglem2  10881  seq3id3  10885  seqhomog  10891  faclbnd  11102  faclbnd3  11104  bcm1k  11121  hashfz1  11144  hashfz  11184  hashfzp1  11187  fiubm  11191  hashfacen  11204  leisorel  11205  wrdexb  11232  wrdsymb  11248  wrdred1hash  11264  lsw0  11268  lswex  11272  ccat0  11280  ccatval2  11282  ccatw2s1leng  11322  ccats1val2  11324  swrds1  11356  swrdlsw  11357  ccats1pfxeqrex  11403  pfxccatin12lem1  11416  swrdccatin2  11417  swrdccat  11423  cats1fvd  11454  s1s2d  11482  s1s3d  11483  cjcj  11564  caucvgre  11662  r19.2uz  11674  resqrexlemgt0  11701  ltabs  11768  xrmaxiflemab  11928  xrmaxiflemlub  11929  nnf1o  12058  summodclem2a  12063  fsumf1o  12072  fisum0diag2  12129  modfsummodlemstep  12139  fsumparts  12152  clim2prod  12221  prodfap0  12227  prodmodclem2a  12258  fprodssdc  12272  fprodcllem  12288  ef0lem  12342  resinval  12397  recosval  12398  demoivreALT  12456  nn0o  12589  gcdmultiplez  12713  dvdssq  12723  nninfct  12733  eucalg  12752  lcmgcdnn  12775  dvdsnprmd  12818  prm2orodd  12819  isprm5lem  12834  qnumdenbi  12885  nn0gcdsq  12893  phibnd  12910  hashdvds  12914  phimullem  12918  prmdiveq  12929  hashgcdlem  12931  modprm0  12948  nnnn0modprm0  12949  modprmn0modprm0  12950  oddprm  12953  prm23lt5  12957  pcprendvds  12984  pcidlem  13017  pcmpt  13037  pcfac  13044  infpnlem2  13054  prmunb  13056  1arith  13061  4sqlem19  13103  unennn  13140  ennnfonelemk  13143  ennnfonelemjn  13145  ennnfonelemhf1o  13156  ennnfonelemex  13157  ennnfonelemf1  13161  ennnfonelemrn  13162  qnnen  13174  unbendc  13197  setsfun0  13240  srngbased  13352  srngplusgd  13353  srngmulrd  13354  srnginvld  13355  lmodbased  13370  lmodplusgd  13371  lmodscad  13372  lmodvscad  13373  ipsbased  13382  ipsaddgd  13383  ipsmulrd  13384  ipsscad  13385  ipsvscad  13386  ipsipd  13387  tgval  13467  prdsbas3  13492  isnsgrp  13611  ismnd  13624  dfgrp2e  13733  subgintm  13907  eqg0el  13938  ecqusaddcl  13948  kerf1ghm  13983  gsumfzconst  14050  imasrng  14092  srgisid  14122  srg1zr  14123  qusring2  14202  oppr1g  14218  dvdsr02  14242  isunitd  14243  crngunit  14248  unitpropdg  14285  elrhmunit  14314  subrngintm  14349  subrguss  14373  subrgunit  14376  subrgugrp  14377  subrgintm  14380  lmodfopnelem1  14464  rmodislmodlem  14490  rmodislmod  14491  lssuni  14503  islss3  14519  lss0v  14570  sraval  14577  rnglidlmmgm  14636  2idllidld  14646  2idlridld  14647  rng2idl0  14659  rng2idlsubg0  14662  zrh0  14765  znle  14777  zndvds0  14790  znf1o  14791  znleval  14793  znfi  14795  znhash  14796  znunit  14799  psrbaglecl  14816  psrbasg  14821  psradd  14826  psr0cl  14828  mpladd  14851  cldval  14956  ntrfval  14957  clsfval  14958  neifval  14997  neif  14998  neival  15000  cnclima  15080  cncnpi  15085  cnrest2  15093  cnrest2r  15094  cnptoprest  15096  cnpdis  15099  txvalex  15111  txval  15112  txcnmpt  15130  txdis  15134  cnmpt1t  15142  cnmpt2t  15150  hmeocnv  15164  hmeontr  15170  txhmeo  15176  xmetunirn  15215  xmettpos  15227  metn0  15235  xmetres  15239  metres  15240  blrnps  15268  blrn  15269  blin2  15289  blbas  15290  xmeterval  15292  xmettxlem  15366  xmettx  15367  metcnpi  15372  reldvg  15536  dvaddxx  15560  dvmulxx  15561  dviaddf  15562  dvimulf  15563  dvfre  15567  dvmptid  15573  dveflem  15583  elply2  15592  plyreres  15621  sinq12gt0  15687  rprelogbdiv  15814  logbgcd1irr  15824  fsumdvdsmul  15851  lgslem4  15868  lgsdirprm  15899  gausslemma2dlem0a  15914  gausslemma2dlem0f  15919  gausslemma2dlem0i  15922  gausslemma2dlem1a  15923  gausslemma2dlem1cl  15924  gausslemma2dlem5  15931  gausslemma2dlem6  15932  gausslemma2d  15934  lgseisenlem1  15935  lgseisenlem2  15936  lgseisenlem3  15937  lgseisen  15939  lgsquadlem1  15942  m1lgs  15950  2lgslem1a  15953  2lgslem1c  15955  2lgsoddprmlem2  15971  edgval  16047  edgstruct  16051  umgrnloopv  16101  umgredgprv  16102  upgr1edc  16108  umgredgne  16137  usgredgssen  16149  umgr2edg1  16196  uspgredg2vlem  16207  uspgr1edc  16227  uhgrspansubgrlem  16263  wlkm  16326  wlkvtxiedg  16332  wlkvtxiedgg  16333  wlk1walkdom  16346  g0wlk0  16357  wlkres  16366  trlf1  16375  trlreslem  16376  trlres  16377  clwwlkg  16380  clwwlkccatlem  16387  clwwlknon  16416  eupthfi  16438  eupthseg  16439  eupthres  16444  trlsegvdeglem1  16447  trlsegvdeglem7  16453  trlsegvdegfi  16454  eupth2lem3lem2fi  16456  eupth2lem3lem3fi  16457  eupth2lem3lem6fi  16458  eupth2lem3lem4fi  16460  eupth2lem3lem7fi  16461  eupth2lem3fi  16463  eupth2lemsfi  16465  eupth2fi  16466  konigsbergssiedgwen  16473  bj-inex  16669  bj-sucexg  16684  bj-peano4  16717  setindis  16729  bdsetindis  16731  bj-inf2vnlem1  16732  nnsf  16775  nninfall  16779  nninfsellemeq  16784  sbthom  16798  gfsumval  16853