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  384  hbim  1538  nfal  1569  19.9hd  1655  equsexd  1722  sbcof2  1803  aev  1805  sbequi  1832  nfsbd  1970  mo2n  2047  eupickb  2100  r19.29af2  2610  spc2gv  2821  spc3gv  2823  eqvincg  2854  sbcco3g  3106  ssrmof  3210  exmidsssnc  4189  snelpwi  4197  opth1  4221  frind  4337  onin  4371  abnexg  4431  reusv1  4443  xpexg  4725  dmexg  4875  rnexg  4876  relfld  5139  funimaexglem  5281  funimaexg  5282  fabexg  5385  fsnd  5485  nfvres  5529  funimass4  5547  elfvmptrab1  5590  funconstss  5614  f1oresrab  5661  resfunexg  5717  f1eqcocnv  5770  isores1  5793  isoini  5797  isose  5800  isopolem  5801  isosolem  5803  eusvobj2  5839  acexmidlemcase  5848  oprabid  5885  offval  6068  resfunexgALT  6087  offval3  6113  1stvalg  6121  2ndvalg  6122  1stcof  6142  2ndcof  6143  cnvf1o  6204  tposf12  6248  smores3  6272  smoiso  6281  tfr0dm  6301  tfrlemibxssdm  6306  tfrlemi14d  6312  tfrexlem  6313  tfr1onlemssrecs  6318  tfr1onlemsucfn  6319  tfr1onlemsucaccv  6320  tfr1onlembxssdm  6322  tfr1onlemres  6328  tfri1dALT  6330  tfrcllemssrecs  6331  tfrcllemsucfn  6332  tfrcllemsucaccv  6333  tfrcllembxssdm  6335  tfrcllemres  6341  rdgss  6362  nnsucsssuc  6471  nntr2  6482  swoord1  6542  swoord2  6543  iinerm  6585  eroveu  6604  pmresg  6654  en1uniel  6782  fopwdom  6814  xpen  6823  ssenen  6829  isinfinf  6875  ac6sfi  6876  preimaf1ofi  6928  sbthlem1  6934  fi0  6952  fiss  6954  supubti  6976  suplubti  6977  isotilem  6983  supisolem  6985  supisoex  6986  supisoti  6987  ordiso2  7012  eldju1st  7048  eldju2ndl  7049  updjud  7059  djudom  7070  ctmlemr  7085  enumctlemm  7091  nnnninfeq  7104  ctssexmid  7126  nninfwlpoimlemginf  7152  exmidonfinlem  7170  en2other2  7173  exmidaclem  7185  cc2lem  7228  cc3  7230  addclnq  7337  mulclnq  7338  1qec  7350  prarloclemarch2  7381  enq0tr  7396  addclnq0  7413  mulclnq0  7414  nq0m0r  7418  prarloclemlo  7456  prarloc  7465  genpml  7479  genpmu  7480  addnqprl  7491  addnqpru  7492  recnnpr  7510  prmuloc2  7529  1idpru  7553  ltexprlemm  7562  ltexprlemloc  7569  recexprlemm  7586  recexprlem1ssl  7595  caucvgprlemnkj  7628  caucvgprlemnbj  7629  caucvgprlemm  7630  caucvgprlemopl  7631  caucvgprlemlol  7632  caucvgprlemladdfu  7639  caucvgprlemladdrl  7640  caucvgprprlemk  7645  caucvgprprlemloccalc  7646  caucvgprprlemnkltj  7651  caucvgprprlemnjltk  7653  caucvgprprlemml  7656  caucvgprprlemmu  7657  caucvgprprlemlol  7660  caucvgprprlemexb  7669  caucvgprprlem1  7671  suplocexprlemml  7678  suplocexprlemlub  7686  addclsr  7715  mulclsr  7716  prsrcl  7746  caucvgsrlemoffcau  7760  peano5nnnn  7854  mulap0r  8534  nn1suc  8897  prime  9311  zindd  9330  xrlttri3  9754  xnn0xadd0  9824  fzopth  10017  fzsuc  10025  fzpred  10026  fzp1ss  10029  fztp  10034  fseq1p1m1  10050  1fv  10095  elfzom1elp1fzo  10158  ssfzo12  10180  fzosplitsn  10189  divfl0  10252  modqid  10305  modqmuladdim  10323  frecuzrdgtcl  10368  frecuzrdgfunlem  10375  frecfzennn  10382  frecfzen2  10383  seq3val  10414  seqvalcd  10415  iseqf1olemqcl  10442  iseqf1olemnab  10444  iseqf1olemmo  10448  iseqf1olemqk  10450  seq3f1olemstep  10457  seq3id3  10463  faclbnd  10675  faclbnd3  10677  bcm1k  10694  hashfz1  10717  focdmex  10721  hashfz  10756  hashfzp1  10759  fiubm  10763  hashfacen  10771  leisorel  10772  cjcj  10847  caucvgre  10945  r19.2uz  10957  resqrexlemgt0  10984  ltabs  11051  xrmaxiflemab  11210  xrmaxiflemlub  11211  nnf1o  11339  summodclem2a  11344  fsumf1o  11353  fisum0diag2  11410  modfsummodlemstep  11420  fsumparts  11433  clim2prod  11502  prodfap0  11508  prodmodclem2a  11539  fprodssdc  11553  fprodcllem  11569  ef0lem  11623  resinval  11678  recosval  11679  demoivreALT  11736  nn0o  11866  zsupcllemstep  11900  zsupcllemex  11901  infssuzledc  11905  gcdmultiplez  11976  dvdssq  11986  eucalg  12013  lcmgcdnn  12036  dvdsnprmd  12079  prm2orodd  12080  isprm5lem  12095  qnumdenbi  12146  nn0gcdsq  12154  phibnd  12171  hashdvds  12175  phimullem  12179  prmdiveq  12190  hashgcdlem  12192  modprm0  12208  nnnn0modprm0  12209  modprmn0modprm0  12210  oddprm  12213  prm23lt5  12217  pcprendvds  12244  pcidlem  12276  pcmpt  12295  pcfac  12302  infpnlem2  12312  prmunb  12314  1arith  12319  unennn  12352  ennnfonelemk  12355  ennnfonelemjn  12357  ennnfonelemhf1o  12368  ennnfonelemex  12369  ennnfonelemf1  12373  ennnfonelemrn  12374  qnnen  12386  unbendc  12409  setsfun0  12452  srngbased  12541  srngplusgd  12542  srngmulrd  12543  srnginvld  12544  lmodbased  12552  lmodplusgd  12553  lmodscad  12554  lmodvscad  12555  ipsbased  12560  ipsaddgd  12561  ipsmulrd  12562  ipsscad  12563  ipsvscad  12564  ipsipd  12565  isnsgrp  12647  ismnd  12655  dfgrp2e  12733  tgval  12843  cldval  12893  ntrfval  12894  clsfval  12895  neifval  12934  neif  12935  neival  12937  cnclima  13017  cncnpi  13022  cnrest2  13030  cnrest2r  13031  cnptoprest  13033  cnpdis  13036  txvalex  13048  txval  13049  txcnmpt  13067  txdis  13071  cnmpt1t  13079  cnmpt2t  13087  hmeocnv  13101  hmeontr  13107  txhmeo  13113  xmetunirn  13152  xmettpos  13164  metn0  13172  xmetres  13176  metres  13177  blrnps  13205  blrn  13206  blin2  13226  blbas  13227  xmeterval  13229  xmettxlem  13303  xmettx  13304  metcnpi  13309  reldvg  13442  dvaddxx  13461  dvmulxx  13462  dviaddf  13463  dvimulf  13464  dvfre  13468  dveflem  13481  sinq12gt0  13545  rprelogbdiv  13669  logbgcd1irr  13679  lgslem4  13698  lgsdirprm  13729  bj-inex  13942  bj-sucexg  13957  bj-peano4  13990  setindis  14002  bdsetindis  14004  bj-inf2vnlem1  14005  exmid1stab  14033  nnsf  14038  nninfall  14042  nninfsellemeq  14047  sbthom  14058