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  4287  exmid1stab  4292  snelpwi  4297  opth1  4322  frind  4443  onin  4477  abnexg  4537  reusv1  4549  xpexg  4833  reldmm  4942  dmexg  4988  rnexg  4989  elrelimasn  5094  relfld  5257  funimaexglem  5404  funimaexg  5405  fabexg  5515  fsnd  5618  elfvm  5662  nfvres  5665  funimass4  5686  elfvmptrab1  5731  funconstss  5755  f1oresrab  5802  resfunexg  5864  f1eqcocnv  5921  isores1  5944  isoini  5948  isose  5951  isopolem  5952  isosolem  5954  eusvobj2  5993  acexmidlemcase  6002  oprabid  6039  offval  6232  resfunexgALT  6259  offval3  6285  1stvalg  6294  2ndvalg  6295  1stcof  6315  2ndcof  6316  cnvf1o  6377  tposf12  6421  smores3  6445  smoiso  6454  tfr0dm  6474  tfrlemibxssdm  6479  tfrlemi14d  6485  tfrexlem  6486  tfr1onlemssrecs  6491  tfr1onlemsucfn  6492  tfr1onlemsucaccv  6493  tfr1onlembxssdm  6495  tfr1onlemres  6501  tfri1dALT  6503  tfrcllemssrecs  6504  tfrcllemsucfn  6505  tfrcllemsucaccv  6506  tfrcllembxssdm  6508  tfrcllemres  6514  rdgss  6535  nnsucsssuc  6646  nntr2  6657  swoord1  6717  swoord2  6718  iinerm  6762  eroveu  6781  pmresg  6831  en1uniel  6964  dom1o  6985  pw2f1odclem  7003  fopwdom  7005  xpen  7014  ssenen  7020  isinfinf  7067  ac6sfi  7068  preimaf1ofi  7126  sbthlem1  7132  fi0  7150  fiss  7152  supubti  7174  suplubti  7175  isotilem  7181  supisolem  7183  supisoex  7184  supisoti  7185  ordiso2  7210  eldju1st  7246  eldju2ndl  7247  updjud  7257  djudom  7268  ctmlemr  7283  enumctlemm  7289  nnnninfeq  7303  ctssexmid  7325  nninfwlpoimlemginf  7351  exmidonfinlem  7379  en2other2  7382  exmidaclem  7398  cc2lem  7460  cc3  7462  addclnq  7570  mulclnq  7571  1qec  7583  prarloclemarch2  7614  enq0tr  7629  addclnq0  7646  mulclnq0  7647  nq0m0r  7651  prarloclemlo  7689  prarloc  7698  genpml  7712  genpmu  7713  addnqprl  7724  addnqpru  7725  recnnpr  7743  prmuloc2  7762  1idpru  7786  ltexprlemm  7795  ltexprlemloc  7802  recexprlemm  7819  recexprlem1ssl  7828  caucvgprlemnkj  7861  caucvgprlemnbj  7862  caucvgprlemm  7863  caucvgprlemopl  7864  caucvgprlemlol  7865  caucvgprlemladdfu  7872  caucvgprlemladdrl  7873  caucvgprprlemk  7878  caucvgprprlemloccalc  7879  caucvgprprlemnkltj  7884  caucvgprprlemnjltk  7886  caucvgprprlemml  7889  caucvgprprlemmu  7890  caucvgprprlemlol  7893  caucvgprprlemexb  7902  caucvgprprlem1  7904  suplocexprlemml  7911  suplocexprlemlub  7919  addclsr  7948  mulclsr  7949  prsrcl  7979  caucvgsrlemoffcau  7993  peano5nnnn  8087  mulap0r  8770  nn1suc  9137  prime  9554  zindd  9573  xrlttri3  10001  xnn0xadd0  10071  fzopth  10265  fzsuc  10273  fzpred  10274  fzp1ss  10277  fztp  10282  fseq1p1m1  10298  1fv  10343  elfzom1elp1fzo  10416  ssfzo12  10438  fzosplitsn  10447  zsupcllemstep  10457  zsupcllemex  10458  infssuzledc  10462  divfl0  10524  fldiv4lem1div2uz2  10534  modqid  10579  modqmuladdim  10597  frecuzrdgtcl  10642  frecuzrdgfunlem  10649  frecfzennn  10656  frecfzen2  10657  seq3val  10690  seqvalcd  10691  seqsplitg  10719  iseqf1olemqcl  10729  iseqf1olemnab  10731  iseqf1olemmo  10735  iseqf1olemqk  10737  seq3f1olemstep  10744  seqf1oglem2  10750  seq3id3  10754  seqhomog  10760  faclbnd  10971  faclbnd3  10973  bcm1k  10990  hashfz1  11013  hashfz  11051  hashfzp1  11054  fiubm  11058  hashfacen  11066  leisorel  11067  wrdexb  11091  wrdsymb  11107  wrdred1hash  11123  lsw0  11127  lswex  11131  ccat0  11139  ccatval2  11141  ccats1val2  11179  swrds1  11208  swrdlsw  11209  ccats1pfxeqrex  11255  pfxccatin12lem1  11268  swrdccatin2  11269  swrdccat  11275  cats1fvd  11306  cjcj  11402  caucvgre  11500  r19.2uz  11512  resqrexlemgt0  11539  ltabs  11606  xrmaxiflemab  11766  xrmaxiflemlub  11767  nnf1o  11895  summodclem2a  11900  fsumf1o  11909  fisum0diag2  11966  modfsummodlemstep  11976  fsumparts  11989  clim2prod  12058  prodfap0  12064  prodmodclem2a  12095  fprodssdc  12109  fprodcllem  12125  ef0lem  12179  resinval  12234  recosval  12235  demoivreALT  12293  nn0o  12426  gcdmultiplez  12550  dvdssq  12560  nninfct  12570  eucalg  12589  lcmgcdnn  12612  dvdsnprmd  12655  prm2orodd  12656  isprm5lem  12671  qnumdenbi  12722  nn0gcdsq  12730  phibnd  12747  hashdvds  12751  phimullem  12755  prmdiveq  12766  hashgcdlem  12768  modprm0  12785  nnnn0modprm0  12786  modprmn0modprm0  12787  oddprm  12790  prm23lt5  12794  pcprendvds  12821  pcidlem  12854  pcmpt  12874  pcfac  12881  infpnlem2  12891  prmunb  12893  1arith  12898  4sqlem19  12940  unennn  12976  ennnfonelemk  12979  ennnfonelemjn  12981  ennnfonelemhf1o  12992  ennnfonelemex  12993  ennnfonelemf1  12997  ennnfonelemrn  12998  qnnen  13010  unbendc  13033  setsfun0  13076  srngbased  13188  srngplusgd  13189  srngmulrd  13190  srnginvld  13191  lmodbased  13206  lmodplusgd  13207  lmodscad  13208  lmodvscad  13209  ipsbased  13218  ipsaddgd  13219  ipsmulrd  13220  ipsscad  13221  ipsvscad  13222  ipsipd  13223  tgval  13303  prdsbas3  13328  isnsgrp  13447  ismnd  13460  dfgrp2e  13569  subgintm  13743  eqg0el  13774  ecqusaddcl  13784  kerf1ghm  13819  gsumfzconst  13886  imasrng  13927  srgisid  13957  srg1zr  13958  qusring2  14037  oppr1g  14053  dvdsr02  14077  isunitd  14078  crngunit  14083  unitpropdg  14120  elrhmunit  14149  subrngintm  14184  subrguss  14208  subrgunit  14211  subrgugrp  14212  subrgintm  14215  lmodfopnelem1  14296  rmodislmodlem  14322  rmodislmod  14323  lssuni  14335  islss3  14351  lss0v  14402  sraval  14409  rnglidlmmgm  14468  2idllidld  14478  2idlridld  14479  rng2idl0  14491  rng2idlsubg0  14494  zrh0  14597  znle  14609  zndvds0  14622  znf1o  14623  znleval  14625  znfi  14627  znhash  14628  znunit  14631  psrbasg  14646  psradd  14651  psr0cl  14653  mpladd  14676  cldval  14781  ntrfval  14782  clsfval  14783  neifval  14822  neif  14823  neival  14825  cnclima  14905  cncnpi  14910  cnrest2  14918  cnrest2r  14919  cnptoprest  14921  cnpdis  14924  txvalex  14936  txval  14937  txcnmpt  14955  txdis  14959  cnmpt1t  14967  cnmpt2t  14975  hmeocnv  14989  hmeontr  14995  txhmeo  15001  xmetunirn  15040  xmettpos  15052  metn0  15060  xmetres  15064  metres  15065  blrnps  15093  blrn  15094  blin2  15114  blbas  15115  xmeterval  15117  xmettxlem  15191  xmettx  15192  metcnpi  15197  reldvg  15361  dvaddxx  15385  dvmulxx  15386  dviaddf  15387  dvimulf  15388  dvfre  15392  dvmptid  15398  dveflem  15408  elply2  15417  plyreres  15446  sinq12gt0  15512  rprelogbdiv  15639  logbgcd1irr  15649  fsumdvdsmul  15673  lgslem4  15690  lgsdirprm  15721  gausslemma2dlem0a  15736  gausslemma2dlem0f  15741  gausslemma2dlem0i  15744  gausslemma2dlem1a  15745  gausslemma2dlem1cl  15746  gausslemma2dlem5  15753  gausslemma2dlem6  15754  gausslemma2d  15756  lgseisenlem1  15757  lgseisenlem2  15758  lgseisenlem3  15759  lgseisen  15761  lgsquadlem1  15764  m1lgs  15772  2lgslem1a  15775  2lgslem1c  15777  2lgsoddprmlem2  15793  edgstruct  15872  umgrnloopv  15922  umgredgprv  15923  upgr1edc  15929  umgredgne  15956  usgredgssen  15968  umgr2edg1  16015  uspgredg2vlem  16026  wlkm  16060  wlkvtxiedg  16066  wlkvtxiedgg  16067  wlk1walkdom  16080  g0wlk0  16091  wlkres  16098  trlf1  16106  trlreslem  16107  trlres  16108  bj-inex  16294  bj-sucexg  16309  bj-peano4  16342  setindis  16354  bdsetindis  16356  bj-inf2vnlem1  16357  nnsf  16401  nninfall  16405  nninfsellemeq  16410  sbthom  16424