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  4288  exmid1stab  4293  snelpwi  4298  opth1  4323  frind  4444  onin  4478  abnexg  4538  reusv1  4550  xpexg  4835  reldmm  4945  dmexg  4991  rnexg  4992  elrelimasn  5097  relfld  5260  funimaexglem  5407  funimaexg  5408  fabexg  5518  fsnd  5621  elfvm  5665  nfvres  5668  funimass4  5689  elfvmptrab1  5734  funconstss  5758  f1oresrab  5805  resfunexg  5867  f1eqcocnv  5924  isores1  5947  isoini  5951  isose  5954  isopolem  5955  isosolem  5957  eusvobj2  5996  acexmidlemcase  6005  oprabid  6042  offval  6235  resfunexgALT  6262  offval3  6288  1stvalg  6297  2ndvalg  6298  1stcof  6318  2ndcof  6319  cnvf1o  6382  tposf12  6426  smores3  6450  smoiso  6459  tfr0dm  6479  tfrlemibxssdm  6484  tfrlemi14d  6490  tfrexlem  6491  tfr1onlemssrecs  6496  tfr1onlemsucfn  6497  tfr1onlemsucaccv  6498  tfr1onlembxssdm  6500  tfr1onlemres  6506  tfri1dALT  6508  tfrcllemssrecs  6509  tfrcllemsucfn  6510  tfrcllemsucaccv  6511  tfrcllembxssdm  6513  tfrcllemres  6519  rdgss  6540  nnsucsssuc  6651  nntr2  6662  swoord1  6722  swoord2  6723  iinerm  6767  eroveu  6786  pmresg  6836  en1uniel  6969  dom1o  6990  pw2f1odclem  7008  fopwdom  7010  xpen  7019  ssenen  7025  isinfinf  7072  ac6sfi  7073  preimaf1ofi  7134  sbthlem1  7140  fi0  7158  fiss  7160  supubti  7182  suplubti  7183  isotilem  7189  supisolem  7191  supisoex  7192  supisoti  7193  ordiso2  7218  eldju1st  7254  eldju2ndl  7255  updjud  7265  djudom  7276  ctmlemr  7291  enumctlemm  7297  nnnninfeq  7311  ctssexmid  7333  nninfwlpoimlemginf  7359  exmidonfinlem  7387  en2other2  7390  exmidaclem  7406  cc2lem  7468  cc3  7470  addclnq  7578  mulclnq  7579  1qec  7591  prarloclemarch2  7622  enq0tr  7637  addclnq0  7654  mulclnq0  7655  nq0m0r  7659  prarloclemlo  7697  prarloc  7706  genpml  7720  genpmu  7721  addnqprl  7732  addnqpru  7733  recnnpr  7751  prmuloc2  7770  1idpru  7794  ltexprlemm  7803  ltexprlemloc  7810  recexprlemm  7827  recexprlem1ssl  7836  caucvgprlemnkj  7869  caucvgprlemnbj  7870  caucvgprlemm  7871  caucvgprlemopl  7872  caucvgprlemlol  7873  caucvgprlemladdfu  7880  caucvgprlemladdrl  7881  caucvgprprlemk  7886  caucvgprprlemloccalc  7887  caucvgprprlemnkltj  7892  caucvgprprlemnjltk  7894  caucvgprprlemml  7897  caucvgprprlemmu  7898  caucvgprprlemlol  7901  caucvgprprlemexb  7910  caucvgprprlem1  7912  suplocexprlemml  7919  suplocexprlemlub  7927  addclsr  7956  mulclsr  7957  prsrcl  7987  caucvgsrlemoffcau  8001  peano5nnnn  8095  mulap0r  8778  nn1suc  9145  prime  9562  zindd  9581  xrlttri3  10010  xnn0xadd0  10080  fzopth  10274  fzsuc  10282  fzpred  10283  fzp1ss  10286  fztp  10291  fseq1p1m1  10307  1fv  10352  elfzom1elp1fzo  10425  ssfzo12  10447  fzosplitsn  10456  zsupcllemstep  10466  zsupcllemex  10467  infssuzledc  10471  divfl0  10533  fldiv4lem1div2uz2  10543  modqid  10588  modqmuladdim  10606  frecuzrdgtcl  10651  frecuzrdgfunlem  10658  frecfzennn  10665  frecfzen2  10666  seq3val  10699  seqvalcd  10700  seqsplitg  10728  iseqf1olemqcl  10738  iseqf1olemnab  10740  iseqf1olemmo  10744  iseqf1olemqk  10746  seq3f1olemstep  10753  seqf1oglem2  10759  seq3id3  10763  seqhomog  10769  faclbnd  10980  faclbnd3  10982  bcm1k  10999  hashfz1  11022  hashfz  11061  hashfzp1  11064  fiubm  11068  hashfacen  11076  leisorel  11077  wrdexb  11101  wrdsymb  11117  wrdred1hash  11133  lsw0  11137  lswex  11141  ccat0  11149  ccatval2  11151  ccats1val2  11192  swrds1  11221  swrdlsw  11222  ccats1pfxeqrex  11268  pfxccatin12lem1  11281  swrdccatin2  11282  swrdccat  11288  cats1fvd  11319  cjcj  11415  caucvgre  11513  r19.2uz  11525  resqrexlemgt0  11552  ltabs  11619  xrmaxiflemab  11779  xrmaxiflemlub  11780  nnf1o  11908  summodclem2a  11913  fsumf1o  11922  fisum0diag2  11979  modfsummodlemstep  11989  fsumparts  12002  clim2prod  12071  prodfap0  12077  prodmodclem2a  12108  fprodssdc  12122  fprodcllem  12138  ef0lem  12192  resinval  12247  recosval  12248  demoivreALT  12306  nn0o  12439  gcdmultiplez  12563  dvdssq  12573  nninfct  12583  eucalg  12602  lcmgcdnn  12625  dvdsnprmd  12668  prm2orodd  12669  isprm5lem  12684  qnumdenbi  12735  nn0gcdsq  12743  phibnd  12760  hashdvds  12764  phimullem  12768  prmdiveq  12779  hashgcdlem  12781  modprm0  12798  nnnn0modprm0  12799  modprmn0modprm0  12800  oddprm  12803  prm23lt5  12807  pcprendvds  12834  pcidlem  12867  pcmpt  12887  pcfac  12894  infpnlem2  12904  prmunb  12906  1arith  12911  4sqlem19  12953  unennn  12989  ennnfonelemk  12992  ennnfonelemjn  12994  ennnfonelemhf1o  13005  ennnfonelemex  13006  ennnfonelemf1  13010  ennnfonelemrn  13011  qnnen  13023  unbendc  13046  setsfun0  13089  srngbased  13201  srngplusgd  13202  srngmulrd  13203  srnginvld  13204  lmodbased  13219  lmodplusgd  13220  lmodscad  13221  lmodvscad  13222  ipsbased  13231  ipsaddgd  13232  ipsmulrd  13233  ipsscad  13234  ipsvscad  13235  ipsipd  13236  tgval  13316  prdsbas3  13341  isnsgrp  13460  ismnd  13473  dfgrp2e  13582  subgintm  13756  eqg0el  13787  ecqusaddcl  13797  kerf1ghm  13832  gsumfzconst  13899  imasrng  13940  srgisid  13970  srg1zr  13971  qusring2  14050  oppr1g  14066  dvdsr02  14090  isunitd  14091  crngunit  14096  unitpropdg  14133  elrhmunit  14162  subrngintm  14197  subrguss  14221  subrgunit  14224  subrgugrp  14225  subrgintm  14228  lmodfopnelem1  14309  rmodislmodlem  14335  rmodislmod  14336  lssuni  14348  islss3  14364  lss0v  14415  sraval  14422  rnglidlmmgm  14481  2idllidld  14491  2idlridld  14492  rng2idl0  14504  rng2idlsubg0  14507  zrh0  14610  znle  14622  zndvds0  14635  znf1o  14636  znleval  14638  znfi  14640  znhash  14641  znunit  14644  psrbasg  14659  psradd  14664  psr0cl  14666  mpladd  14689  cldval  14794  ntrfval  14795  clsfval  14796  neifval  14835  neif  14836  neival  14838  cnclima  14918  cncnpi  14923  cnrest2  14931  cnrest2r  14932  cnptoprest  14934  cnpdis  14937  txvalex  14949  txval  14950  txcnmpt  14968  txdis  14972  cnmpt1t  14980  cnmpt2t  14988  hmeocnv  15002  hmeontr  15008  txhmeo  15014  xmetunirn  15053  xmettpos  15065  metn0  15073  xmetres  15077  metres  15078  blrnps  15106  blrn  15107  blin2  15127  blbas  15128  xmeterval  15130  xmettxlem  15204  xmettx  15205  metcnpi  15210  reldvg  15374  dvaddxx  15398  dvmulxx  15399  dviaddf  15400  dvimulf  15401  dvfre  15405  dvmptid  15411  dveflem  15421  elply2  15430  plyreres  15459  sinq12gt0  15525  rprelogbdiv  15652  logbgcd1irr  15662  fsumdvdsmul  15686  lgslem4  15703  lgsdirprm  15734  gausslemma2dlem0a  15749  gausslemma2dlem0f  15754  gausslemma2dlem0i  15757  gausslemma2dlem1a  15758  gausslemma2dlem1cl  15759  gausslemma2dlem5  15766  gausslemma2dlem6  15767  gausslemma2d  15769  lgseisenlem1  15770  lgseisenlem2  15771  lgseisenlem3  15772  lgseisen  15774  lgsquadlem1  15777  m1lgs  15785  2lgslem1a  15788  2lgslem1c  15790  2lgsoddprmlem2  15806  edgstruct  15885  umgrnloopv  15935  umgredgprv  15936  upgr1edc  15942  umgredgne  15969  usgredgssen  15981  umgr2edg1  16028  uspgredg2vlem  16039  uspgr1edc  16059  wlkm  16111  wlkvtxiedg  16117  wlkvtxiedgg  16118  wlk1walkdom  16131  g0wlk0  16142  wlkres  16149  trlf1  16157  trlreslem  16158  trlres  16159  clwwlkg  16162  clwwlkccatlem  16169  bj-inex  16379  bj-sucexg  16394  bj-peano4  16427  setindis  16439  bdsetindis  16441  bj-inf2vnlem1  16442  nnsf  16485  nninfall  16489  nninfsellemeq  16494  sbthom  16508