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  1569  nfal  1600  19.9hd  1686  equsexd  1753  sbcof2  1834  aev  1836  sbequi  1863  nfsbd  2006  mo2n  2083  eupickb  2136  r19.29af2  2647  spc2gv  2866  spc3gv  2868  eqvincg  2899  sbcco3g  3153  ssrmof  3258  exmidsssnc  4252  exmid1stab  4257  snelpwi  4261  opth1  4285  frind  4404  onin  4438  abnexg  4498  reusv1  4510  xpexg  4794  dmexg  4948  rnexg  4949  elrelimasn  5054  relfld  5217  funimaexglem  5363  funimaexg  5364  fabexg  5472  fsnd  5575  elfvm  5619  nfvres  5620  funimass4  5639  elfvmptrab1  5684  funconstss  5708  f1oresrab  5755  resfunexg  5815  f1eqcocnv  5870  isores1  5893  isoini  5897  isose  5900  isopolem  5901  isosolem  5903  eusvobj2  5940  acexmidlemcase  5949  oprabid  5986  offval  6176  resfunexgALT  6203  offval3  6229  1stvalg  6238  2ndvalg  6239  1stcof  6259  2ndcof  6260  cnvf1o  6321  tposf12  6365  smores3  6389  smoiso  6398  tfr0dm  6418  tfrlemibxssdm  6423  tfrlemi14d  6429  tfrexlem  6430  tfr1onlemssrecs  6435  tfr1onlemsucfn  6436  tfr1onlemsucaccv  6437  tfr1onlembxssdm  6439  tfr1onlemres  6445  tfri1dALT  6447  tfrcllemssrecs  6448  tfrcllemsucfn  6449  tfrcllemsucaccv  6450  tfrcllembxssdm  6452  tfrcllemres  6458  rdgss  6479  nnsucsssuc  6588  nntr2  6599  swoord1  6659  swoord2  6660  iinerm  6704  eroveu  6723  pmresg  6773  en1uniel  6906  pw2f1odclem  6943  fopwdom  6945  xpen  6954  ssenen  6960  isinfinf  7006  ac6sfi  7007  preimaf1ofi  7065  sbthlem1  7071  fi0  7089  fiss  7091  supubti  7113  suplubti  7114  isotilem  7120  supisolem  7122  supisoex  7123  supisoti  7124  ordiso2  7149  eldju1st  7185  eldju2ndl  7186  updjud  7196  djudom  7207  ctmlemr  7222  enumctlemm  7228  nnnninfeq  7242  ctssexmid  7264  nninfwlpoimlemginf  7290  exmidonfinlem  7314  en2other2  7317  exmidaclem  7333  cc2lem  7391  cc3  7393  addclnq  7501  mulclnq  7502  1qec  7514  prarloclemarch2  7545  enq0tr  7560  addclnq0  7577  mulclnq0  7578  nq0m0r  7582  prarloclemlo  7620  prarloc  7629  genpml  7643  genpmu  7644  addnqprl  7655  addnqpru  7656  recnnpr  7674  prmuloc2  7693  1idpru  7717  ltexprlemm  7726  ltexprlemloc  7733  recexprlemm  7750  recexprlem1ssl  7759  caucvgprlemnkj  7792  caucvgprlemnbj  7793  caucvgprlemm  7794  caucvgprlemopl  7795  caucvgprlemlol  7796  caucvgprlemladdfu  7803  caucvgprlemladdrl  7804  caucvgprprlemk  7809  caucvgprprlemloccalc  7810  caucvgprprlemnkltj  7815  caucvgprprlemnjltk  7817  caucvgprprlemml  7820  caucvgprprlemmu  7821  caucvgprprlemlol  7824  caucvgprprlemexb  7833  caucvgprprlem1  7835  suplocexprlemml  7842  suplocexprlemlub  7850  addclsr  7879  mulclsr  7880  prsrcl  7910  caucvgsrlemoffcau  7924  peano5nnnn  8018  mulap0r  8701  nn1suc  9068  prime  9485  zindd  9504  xrlttri3  9932  xnn0xadd0  10002  fzopth  10196  fzsuc  10204  fzpred  10205  fzp1ss  10208  fztp  10213  fseq1p1m1  10229  1fv  10274  elfzom1elp1fzo  10344  ssfzo12  10366  fzosplitsn  10375  zsupcllemstep  10385  zsupcllemex  10386  infssuzledc  10390  divfl0  10452  fldiv4lem1div2uz2  10462  modqid  10507  modqmuladdim  10525  frecuzrdgtcl  10570  frecuzrdgfunlem  10577  frecfzennn  10584  frecfzen2  10585  seq3val  10618  seqvalcd  10619  seqsplitg  10647  iseqf1olemqcl  10657  iseqf1olemnab  10659  iseqf1olemmo  10663  iseqf1olemqk  10665  seq3f1olemstep  10672  seqf1oglem2  10678  seq3id3  10682  seqhomog  10688  faclbnd  10899  faclbnd3  10901  bcm1k  10918  hashfz1  10941  hashfz  10979  hashfzp1  10982  fiubm  10986  hashfacen  10994  leisorel  10995  wrdexb  11019  wrdsymb  11034  wrdred1hash  11050  lsw0  11054  lswex  11058  ccat0  11066  ccatval2  11068  ccats1val2  11106  swrds1  11135  swrdlsw  11136  cjcj  11244  caucvgre  11342  r19.2uz  11354  resqrexlemgt0  11381  ltabs  11448  xrmaxiflemab  11608  xrmaxiflemlub  11609  nnf1o  11737  summodclem2a  11742  fsumf1o  11751  fisum0diag2  11808  modfsummodlemstep  11818  fsumparts  11831  clim2prod  11900  prodfap0  11906  prodmodclem2a  11937  fprodssdc  11951  fprodcllem  11967  ef0lem  12021  resinval  12076  recosval  12077  demoivreALT  12135  nn0o  12268  gcdmultiplez  12392  dvdssq  12402  nninfct  12412  eucalg  12431  lcmgcdnn  12454  dvdsnprmd  12497  prm2orodd  12498  isprm5lem  12513  qnumdenbi  12564  nn0gcdsq  12572  phibnd  12589  hashdvds  12593  phimullem  12597  prmdiveq  12608  hashgcdlem  12610  modprm0  12627  nnnn0modprm0  12628  modprmn0modprm0  12629  oddprm  12632  prm23lt5  12636  pcprendvds  12663  pcidlem  12696  pcmpt  12716  pcfac  12723  infpnlem2  12733  prmunb  12735  1arith  12740  4sqlem19  12782  unennn  12818  ennnfonelemk  12821  ennnfonelemjn  12823  ennnfonelemhf1o  12834  ennnfonelemex  12835  ennnfonelemf1  12839  ennnfonelemrn  12840  qnnen  12852  unbendc  12875  setsfun0  12918  srngbased  13029  srngplusgd  13030  srngmulrd  13031  srnginvld  13032  lmodbased  13047  lmodplusgd  13048  lmodscad  13049  lmodvscad  13050  ipsbased  13059  ipsaddgd  13060  ipsmulrd  13061  ipsscad  13062  ipsvscad  13063  ipsipd  13064  tgval  13144  prdsbas3  13169  isnsgrp  13288  ismnd  13301  dfgrp2e  13410  subgintm  13584  eqg0el  13615  ecqusaddcl  13625  kerf1ghm  13660  gsumfzconst  13727  imasrng  13768  srgisid  13798  srg1zr  13799  qusring2  13878  oppr1g  13894  dvdsr02  13917  isunitd  13918  crngunit  13923  unitpropdg  13960  elrhmunit  13989  subrngintm  14024  subrguss  14048  subrgunit  14051  subrgugrp  14052  subrgintm  14055  lmodfopnelem1  14136  rmodislmodlem  14162  rmodislmod  14163  lssuni  14175  islss3  14191  lss0v  14242  sraval  14249  rnglidlmmgm  14308  2idllidld  14318  2idlridld  14319  rng2idl0  14331  rng2idlsubg0  14334  zrh0  14437  znle  14449  zndvds0  14462  znf1o  14463  znleval  14465  znfi  14467  znhash  14468  znunit  14471  psrbasg  14486  psradd  14491  psr0cl  14493  mpladd  14516  cldval  14621  ntrfval  14622  clsfval  14623  neifval  14662  neif  14663  neival  14665  cnclima  14745  cncnpi  14750  cnrest2  14758  cnrest2r  14759  cnptoprest  14761  cnpdis  14764  txvalex  14776  txval  14777  txcnmpt  14795  txdis  14799  cnmpt1t  14807  cnmpt2t  14815  hmeocnv  14829  hmeontr  14835  txhmeo  14841  xmetunirn  14880  xmettpos  14892  metn0  14900  xmetres  14904  metres  14905  blrnps  14933  blrn  14934  blin2  14954  blbas  14955  xmeterval  14957  xmettxlem  15031  xmettx  15032  metcnpi  15037  reldvg  15201  dvaddxx  15225  dvmulxx  15226  dviaddf  15227  dvimulf  15228  dvfre  15232  dvmptid  15238  dveflem  15248  elply2  15257  plyreres  15286  sinq12gt0  15352  rprelogbdiv  15479  logbgcd1irr  15489  fsumdvdsmul  15513  lgslem4  15530  lgsdirprm  15561  gausslemma2dlem0a  15576  gausslemma2dlem0f  15581  gausslemma2dlem0i  15584  gausslemma2dlem1a  15585  gausslemma2dlem1cl  15586  gausslemma2dlem5  15593  gausslemma2dlem6  15594  gausslemma2d  15596  lgseisenlem1  15597  lgseisenlem2  15598  lgseisenlem3  15599  lgseisen  15601  lgsquadlem1  15604  m1lgs  15612  2lgslem1a  15615  2lgslem1c  15617  2lgsoddprmlem2  15633  edgstruct  15710  umgrnloopvv  15760  upgr1edc  15764  bj-inex  15957  bj-sucexg  15972  bj-peano4  16005  setindis  16017  bdsetindis  16019  bj-inf2vnlem1  16020  dom1o  16043  nnsf  16057  nninfall  16061  nninfsellemeq  16066  sbthom  16080