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  1533  nfal  1564  19.9hd  1650  equsexd  1717  sbcof2  1798  aev  1800  sbequi  1827  nfsbd  1965  mo2n  2042  eupickb  2095  r19.29af2  2606  spc2gv  2817  spc3gv  2819  eqvincg  2850  sbcco3g  3102  ssrmof  3205  exmidsssnc  4182  snelpwi  4190  opth1  4214  frind  4330  onin  4364  abnexg  4424  reusv1  4436  xpexg  4718  dmexg  4868  rnexg  4869  relfld  5132  funimaexglem  5271  funimaexg  5272  fabexg  5375  fsnd  5475  nfvres  5519  funimass4  5537  elfvmptrab1  5580  funconstss  5603  f1oresrab  5650  resfunexg  5706  f1eqcocnv  5759  isores1  5782  isoini  5786  isose  5789  isopolem  5790  isosolem  5792  eusvobj2  5828  acexmidlemcase  5837  oprabid  5874  offval  6057  resfunexgALT  6076  offval3  6102  1stvalg  6110  2ndvalg  6111  1stcof  6131  2ndcof  6132  cnvf1o  6193  tposf12  6237  smores3  6261  smoiso  6270  tfr0dm  6290  tfrlemibxssdm  6295  tfrlemi14d  6301  tfrexlem  6302  tfr1onlemssrecs  6307  tfr1onlemsucfn  6308  tfr1onlemsucaccv  6309  tfr1onlembxssdm  6311  tfr1onlemres  6317  tfri1dALT  6319  tfrcllemssrecs  6320  tfrcllemsucfn  6321  tfrcllemsucaccv  6322  tfrcllembxssdm  6324  tfrcllemres  6330  rdgss  6351  nnsucsssuc  6460  nntr2  6471  swoord1  6530  swoord2  6531  iinerm  6573  eroveu  6592  pmresg  6642  en1uniel  6770  fopwdom  6802  xpen  6811  ssenen  6817  isinfinf  6863  ac6sfi  6864  preimaf1ofi  6916  sbthlem1  6922  fi0  6940  fiss  6942  supubti  6964  suplubti  6965  isotilem  6971  supisolem  6973  supisoex  6974  supisoti  6975  ordiso2  7000  eldju1st  7036  eldju2ndl  7037  updjud  7047  djudom  7058  ctmlemr  7073  enumctlemm  7079  nnnninfeq  7092  ctssexmid  7114  exmidonfinlem  7149  en2other2  7152  exmidaclem  7164  cc2lem  7207  cc3  7209  addclnq  7316  mulclnq  7317  1qec  7329  prarloclemarch2  7360  enq0tr  7375  addclnq0  7392  mulclnq0  7393  nq0m0r  7397  prarloclemlo  7435  prarloc  7444  genpml  7458  genpmu  7459  addnqprl  7470  addnqpru  7471  recnnpr  7489  prmuloc2  7508  1idpru  7532  ltexprlemm  7541  ltexprlemloc  7548  recexprlemm  7565  recexprlem1ssl  7574  caucvgprlemnkj  7607  caucvgprlemnbj  7608  caucvgprlemm  7609  caucvgprlemopl  7610  caucvgprlemlol  7611  caucvgprlemladdfu  7618  caucvgprlemladdrl  7619  caucvgprprlemk  7624  caucvgprprlemloccalc  7625  caucvgprprlemnkltj  7630  caucvgprprlemnjltk  7632  caucvgprprlemml  7635  caucvgprprlemmu  7636  caucvgprprlemlol  7639  caucvgprprlemexb  7648  caucvgprprlem1  7650  suplocexprlemml  7657  suplocexprlemlub  7665  addclsr  7694  mulclsr  7695  prsrcl  7725  caucvgsrlemoffcau  7739  peano5nnnn  7833  mulap0r  8513  nn1suc  8876  prime  9290  zindd  9309  xrlttri3  9733  xnn0xadd0  9803  fzopth  9996  fzsuc  10004  fzpred  10005  fzp1ss  10008  fztp  10013  fseq1p1m1  10029  1fv  10074  elfzom1elp1fzo  10137  ssfzo12  10159  fzosplitsn  10168  divfl0  10231  modqid  10284  modqmuladdim  10302  frecuzrdgtcl  10347  frecuzrdgfunlem  10354  frecfzennn  10361  frecfzen2  10362  seq3val  10393  seqvalcd  10394  iseqf1olemqcl  10421  iseqf1olemnab  10423  iseqf1olemmo  10427  iseqf1olemqk  10429  seq3f1olemstep  10436  seq3id3  10442  faclbnd  10654  faclbnd3  10656  bcm1k  10673  hashfz1  10696  focdmex  10700  hashfz  10734  hashfzp1  10737  fiubm  10741  hashfacen  10749  leisorel  10750  cjcj  10825  caucvgre  10923  r19.2uz  10935  resqrexlemgt0  10962  ltabs  11029  xrmaxiflemab  11188  xrmaxiflemlub  11189  nnf1o  11317  summodclem2a  11322  fsumf1o  11331  fisum0diag2  11388  modfsummodlemstep  11398  fsumparts  11411  clim2prod  11480  prodfap0  11486  prodmodclem2a  11517  fprodssdc  11531  fprodcllem  11547  ef0lem  11601  resinval  11656  recosval  11657  demoivreALT  11714  nn0o  11844  zsupcllemstep  11878  zsupcllemex  11879  infssuzledc  11883  gcdmultiplez  11954  dvdssq  11964  eucalg  11991  lcmgcdnn  12014  dvdsnprmd  12057  prm2orodd  12058  isprm5lem  12073  qnumdenbi  12124  nn0gcdsq  12132  phibnd  12149  hashdvds  12153  phimullem  12157  prmdiveq  12168  hashgcdlem  12170  modprm0  12186  nnnn0modprm0  12187  modprmn0modprm0  12188  oddprm  12191  prm23lt5  12195  pcprendvds  12222  pcidlem  12254  pcmpt  12273  pcfac  12280  infpnlem2  12290  prmunb  12292  1arith  12297  unennn  12330  ennnfonelemk  12333  ennnfonelemjn  12335  ennnfonelemhf1o  12346  ennnfonelemex  12347  ennnfonelemf1  12351  ennnfonelemrn  12352  qnnen  12364  unbendc  12387  setsfun0  12430  srngbased  12518  srngplusgd  12519  srngmulrd  12520  srnginvld  12521  lmodbased  12529  lmodplusgd  12530  lmodscad  12531  lmodvscad  12532  ipsbased  12537  ipsaddgd  12538  ipsmulrd  12539  ipsscad  12540  ipsvscad  12541  ipsipd  12542  tgval  12689  cldval  12739  ntrfval  12740  clsfval  12741  neifval  12780  neif  12781  neival  12783  cnclima  12863  cncnpi  12868  cnrest2  12876  cnrest2r  12877  cnptoprest  12879  cnpdis  12882  txvalex  12894  txval  12895  txcnmpt  12913  txdis  12917  cnmpt1t  12925  cnmpt2t  12933  hmeocnv  12947  hmeontr  12953  txhmeo  12959  xmetunirn  12998  xmettpos  13010  metn0  13018  xmetres  13022  metres  13023  blrnps  13051  blrn  13052  blin2  13072  blbas  13073  xmeterval  13075  xmettxlem  13149  xmettx  13150  metcnpi  13155  reldvg  13288  dvaddxx  13307  dvmulxx  13308  dviaddf  13309  dvimulf  13310  dvfre  13314  dveflem  13327  sinq12gt0  13391  rprelogbdiv  13515  logbgcd1irr  13525  lgslem4  13544  lgsdirprm  13575  bj-inex  13789  bj-sucexg  13804  bj-peano4  13837  setindis  13849  bdsetindis  13851  bj-inf2vnlem1  13852  exmid1stab  13880  nnsf  13885  nninfall  13889  nninfsellemeq  13894  sbthom  13905