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  1545  nfal  1576  19.9hd  1662  equsexd  1729  sbcof2  1810  aev  1812  sbequi  1839  nfsbd  1977  mo2n  2054  eupickb  2107  r19.29af2  2617  spc2gv  2829  spc3gv  2831  eqvincg  2862  sbcco3g  3115  ssrmof  3219  exmidsssnc  4204  exmid1stab  4209  snelpwi  4213  opth1  4237  frind  4353  onin  4387  abnexg  4447  reusv1  4459  xpexg  4741  dmexg  4892  rnexg  4893  elrelimasn  4995  relfld  5158  funimaexglem  5300  funimaexg  5301  fabexg  5404  fsnd  5505  nfvres  5549  funimass4  5567  elfvmptrab1  5611  funconstss  5635  f1oresrab  5682  resfunexg  5738  f1eqcocnv  5792  isores1  5815  isoini  5819  isose  5822  isopolem  5823  isosolem  5825  eusvobj2  5861  acexmidlemcase  5870  oprabid  5907  offval  6090  resfunexgALT  6109  offval3  6135  1stvalg  6143  2ndvalg  6144  1stcof  6164  2ndcof  6165  cnvf1o  6226  tposf12  6270  smores3  6294  smoiso  6303  tfr0dm  6323  tfrlemibxssdm  6328  tfrlemi14d  6334  tfrexlem  6335  tfr1onlemssrecs  6340  tfr1onlemsucfn  6341  tfr1onlemsucaccv  6342  tfr1onlembxssdm  6344  tfr1onlemres  6350  tfri1dALT  6352  tfrcllemssrecs  6353  tfrcllemsucfn  6354  tfrcllemsucaccv  6355  tfrcllembxssdm  6357  tfrcllemres  6363  rdgss  6384  nnsucsssuc  6493  nntr2  6504  swoord1  6564  swoord2  6565  iinerm  6607  eroveu  6626  pmresg  6676  en1uniel  6804  fopwdom  6836  xpen  6845  ssenen  6851  isinfinf  6897  ac6sfi  6898  preimaf1ofi  6950  sbthlem1  6956  fi0  6974  fiss  6976  supubti  6998  suplubti  6999  isotilem  7005  supisolem  7007  supisoex  7008  supisoti  7009  ordiso2  7034  eldju1st  7070  eldju2ndl  7071  updjud  7081  djudom  7092  ctmlemr  7107  enumctlemm  7113  nnnninfeq  7126  ctssexmid  7148  nninfwlpoimlemginf  7174  exmidonfinlem  7192  en2other2  7195  exmidaclem  7207  cc2lem  7265  cc3  7267  addclnq  7374  mulclnq  7375  1qec  7387  prarloclemarch2  7418  enq0tr  7433  addclnq0  7450  mulclnq0  7451  nq0m0r  7455  prarloclemlo  7493  prarloc  7502  genpml  7516  genpmu  7517  addnqprl  7528  addnqpru  7529  recnnpr  7547  prmuloc2  7566  1idpru  7590  ltexprlemm  7599  ltexprlemloc  7606  recexprlemm  7623  recexprlem1ssl  7632  caucvgprlemnkj  7665  caucvgprlemnbj  7666  caucvgprlemm  7667  caucvgprlemopl  7668  caucvgprlemlol  7669  caucvgprlemladdfu  7676  caucvgprlemladdrl  7677  caucvgprprlemk  7682  caucvgprprlemloccalc  7683  caucvgprprlemnkltj  7688  caucvgprprlemnjltk  7690  caucvgprprlemml  7693  caucvgprprlemmu  7694  caucvgprprlemlol  7697  caucvgprprlemexb  7706  caucvgprprlem1  7708  suplocexprlemml  7715  suplocexprlemlub  7723  addclsr  7752  mulclsr  7753  prsrcl  7783  caucvgsrlemoffcau  7797  peano5nnnn  7891  mulap0r  8572  nn1suc  8938  prime  9352  zindd  9371  xrlttri3  9797  xnn0xadd0  9867  fzopth  10061  fzsuc  10069  fzpred  10070  fzp1ss  10073  fztp  10078  fseq1p1m1  10094  1fv  10139  elfzom1elp1fzo  10202  ssfzo12  10224  fzosplitsn  10233  divfl0  10296  modqid  10349  modqmuladdim  10367  frecuzrdgtcl  10412  frecuzrdgfunlem  10419  frecfzennn  10426  frecfzen2  10427  seq3val  10458  seqvalcd  10459  iseqf1olemqcl  10486  iseqf1olemnab  10488  iseqf1olemmo  10492  iseqf1olemqk  10494  seq3f1olemstep  10501  seq3id3  10507  faclbnd  10721  faclbnd3  10723  bcm1k  10740  hashfz1  10763  hashfz  10801  hashfzp1  10804  fiubm  10808  hashfacen  10816  leisorel  10817  cjcj  10892  caucvgre  10990  r19.2uz  11002  resqrexlemgt0  11029  ltabs  11096  xrmaxiflemab  11255  xrmaxiflemlub  11256  nnf1o  11384  summodclem2a  11389  fsumf1o  11398  fisum0diag2  11455  modfsummodlemstep  11465  fsumparts  11478  clim2prod  11547  prodfap0  11553  prodmodclem2a  11584  fprodssdc  11598  fprodcllem  11614  ef0lem  11668  resinval  11723  recosval  11724  demoivreALT  11781  nn0o  11912  zsupcllemstep  11946  zsupcllemex  11947  infssuzledc  11951  gcdmultiplez  12022  dvdssq  12032  eucalg  12059  lcmgcdnn  12082  dvdsnprmd  12125  prm2orodd  12126  isprm5lem  12141  qnumdenbi  12192  nn0gcdsq  12200  phibnd  12217  hashdvds  12221  phimullem  12225  prmdiveq  12236  hashgcdlem  12238  modprm0  12254  nnnn0modprm0  12255  modprmn0modprm0  12256  oddprm  12259  prm23lt5  12263  pcprendvds  12290  pcidlem  12322  pcmpt  12341  pcfac  12348  infpnlem2  12358  prmunb  12360  1arith  12365  unennn  12398  ennnfonelemk  12401  ennnfonelemjn  12403  ennnfonelemhf1o  12414  ennnfonelemex  12415  ennnfonelemf1  12419  ennnfonelemrn  12420  qnnen  12432  unbendc  12455  setsfun0  12498  srngbased  12605  srngplusgd  12606  srngmulrd  12607  srnginvld  12608  lmodbased  12623  lmodplusgd  12624  lmodscad  12625  lmodvscad  12626  ipsbased  12635  ipsaddgd  12636  ipsmulrd  12637  ipsscad  12638  ipsvscad  12639  ipsipd  12640  tgval  12711  isnsgrp  12812  ismnd  12820  dfgrp2e  12903  subgintm  13058  srgisid  13169  srg1zr  13170  oppr1g  13252  dvdsr02  13274  isunitd  13275  crngunit  13280  unitpropdg  13317  subrguss  13357  subrgunit  13360  subrgugrp  13361  subrgintm  13364  lmodfopnelem1  13414  rmodislmodlem  13440  rmodislmod  13441  cldval  13602  ntrfval  13603  clsfval  13604  neifval  13643  neif  13644  neival  13646  cnclima  13726  cncnpi  13731  cnrest2  13739  cnrest2r  13740  cnptoprest  13742  cnpdis  13745  txvalex  13757  txval  13758  txcnmpt  13776  txdis  13780  cnmpt1t  13788  cnmpt2t  13796  hmeocnv  13810  hmeontr  13816  txhmeo  13822  xmetunirn  13861  xmettpos  13873  metn0  13881  xmetres  13885  metres  13886  blrnps  13914  blrn  13915  blin2  13935  blbas  13936  xmeterval  13938  xmettxlem  14012  xmettx  14013  metcnpi  14018  reldvg  14151  dvaddxx  14170  dvmulxx  14171  dviaddf  14172  dvimulf  14173  dvfre  14177  dveflem  14190  sinq12gt0  14254  rprelogbdiv  14378  logbgcd1irr  14388  lgslem4  14407  lgsdirprm  14438  lgseisenlem1  14453  lgseisenlem2  14454  m1lgs  14455  2lgsoddprmlem2  14457  bj-inex  14662  bj-sucexg  14677  bj-peano4  14710  setindis  14722  bdsetindis  14724  bj-inf2vnlem1  14725  nnsf  14757  nninfall  14761  nninfsellemeq  14766  sbthom  14777