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  2828  spc3gv  2830  eqvincg  2861  sbcco3g  3114  ssrmof  3218  exmidsssnc  4202  exmid1stab  4207  snelpwi  4211  opth1  4235  frind  4351  onin  4385  abnexg  4445  reusv1  4457  xpexg  4739  dmexg  4890  rnexg  4891  elrelimasn  4993  relfld  5156  funimaexglem  5298  funimaexg  5299  fabexg  5402  fsnd  5503  nfvres  5547  funimass4  5565  elfvmptrab1  5609  funconstss  5633  f1oresrab  5680  resfunexg  5736  f1eqcocnv  5789  isores1  5812  isoini  5816  isose  5819  isopolem  5820  isosolem  5822  eusvobj2  5858  acexmidlemcase  5867  oprabid  5904  offval  6087  resfunexgALT  6106  offval3  6132  1stvalg  6140  2ndvalg  6141  1stcof  6161  2ndcof  6162  cnvf1o  6223  tposf12  6267  smores3  6291  smoiso  6300  tfr0dm  6320  tfrlemibxssdm  6325  tfrlemi14d  6331  tfrexlem  6332  tfr1onlemssrecs  6337  tfr1onlemsucfn  6338  tfr1onlemsucaccv  6339  tfr1onlembxssdm  6341  tfr1onlemres  6347  tfri1dALT  6349  tfrcllemssrecs  6350  tfrcllemsucfn  6351  tfrcllemsucaccv  6352  tfrcllembxssdm  6354  tfrcllemres  6360  rdgss  6381  nnsucsssuc  6490  nntr2  6501  swoord1  6561  swoord2  6562  iinerm  6604  eroveu  6623  pmresg  6673  en1uniel  6801  fopwdom  6833  xpen  6842  ssenen  6848  isinfinf  6894  ac6sfi  6895  preimaf1ofi  6947  sbthlem1  6953  fi0  6971  fiss  6973  supubti  6995  suplubti  6996  isotilem  7002  supisolem  7004  supisoex  7005  supisoti  7006  ordiso2  7031  eldju1st  7067  eldju2ndl  7068  updjud  7078  djudom  7089  ctmlemr  7104  enumctlemm  7110  nnnninfeq  7123  ctssexmid  7145  nninfwlpoimlemginf  7171  exmidonfinlem  7189  en2other2  7192  exmidaclem  7204  cc2lem  7262  cc3  7264  addclnq  7371  mulclnq  7372  1qec  7384  prarloclemarch2  7415  enq0tr  7430  addclnq0  7447  mulclnq0  7448  nq0m0r  7452  prarloclemlo  7490  prarloc  7499  genpml  7513  genpmu  7514  addnqprl  7525  addnqpru  7526  recnnpr  7544  prmuloc2  7563  1idpru  7587  ltexprlemm  7596  ltexprlemloc  7603  recexprlemm  7620  recexprlem1ssl  7629  caucvgprlemnkj  7662  caucvgprlemnbj  7663  caucvgprlemm  7664  caucvgprlemopl  7665  caucvgprlemlol  7666  caucvgprlemladdfu  7673  caucvgprlemladdrl  7674  caucvgprprlemk  7679  caucvgprprlemloccalc  7680  caucvgprprlemnkltj  7685  caucvgprprlemnjltk  7687  caucvgprprlemml  7690  caucvgprprlemmu  7691  caucvgprprlemlol  7694  caucvgprprlemexb  7703  caucvgprprlem1  7705  suplocexprlemml  7712  suplocexprlemlub  7720  addclsr  7749  mulclsr  7750  prsrcl  7780  caucvgsrlemoffcau  7794  peano5nnnn  7888  mulap0r  8568  nn1suc  8934  prime  9348  zindd  9367  xrlttri3  9793  xnn0xadd0  9863  fzopth  10056  fzsuc  10064  fzpred  10065  fzp1ss  10068  fztp  10073  fseq1p1m1  10089  1fv  10134  elfzom1elp1fzo  10197  ssfzo12  10219  fzosplitsn  10228  divfl0  10291  modqid  10344  modqmuladdim  10362  frecuzrdgtcl  10407  frecuzrdgfunlem  10414  frecfzennn  10421  frecfzen2  10422  seq3val  10453  seqvalcd  10454  iseqf1olemqcl  10481  iseqf1olemnab  10483  iseqf1olemmo  10487  iseqf1olemqk  10489  seq3f1olemstep  10496  seq3id3  10502  faclbnd  10714  faclbnd3  10716  bcm1k  10733  hashfz1  10756  hashfz  10794  hashfzp1  10797  fiubm  10801  hashfacen  10809  leisorel  10810  cjcj  10885  caucvgre  10983  r19.2uz  10995  resqrexlemgt0  11022  ltabs  11089  xrmaxiflemab  11248  xrmaxiflemlub  11249  nnf1o  11377  summodclem2a  11382  fsumf1o  11391  fisum0diag2  11448  modfsummodlemstep  11458  fsumparts  11471  clim2prod  11540  prodfap0  11546  prodmodclem2a  11577  fprodssdc  11591  fprodcllem  11607  ef0lem  11661  resinval  11716  recosval  11717  demoivreALT  11774  nn0o  11904  zsupcllemstep  11938  zsupcllemex  11939  infssuzledc  11943  gcdmultiplez  12014  dvdssq  12024  eucalg  12051  lcmgcdnn  12074  dvdsnprmd  12117  prm2orodd  12118  isprm5lem  12133  qnumdenbi  12184  nn0gcdsq  12192  phibnd  12209  hashdvds  12213  phimullem  12217  prmdiveq  12228  hashgcdlem  12230  modprm0  12246  nnnn0modprm0  12247  modprmn0modprm0  12248  oddprm  12251  prm23lt5  12255  pcprendvds  12282  pcidlem  12314  pcmpt  12333  pcfac  12340  infpnlem2  12350  prmunb  12352  1arith  12357  unennn  12390  ennnfonelemk  12393  ennnfonelemjn  12395  ennnfonelemhf1o  12406  ennnfonelemex  12407  ennnfonelemf1  12411  ennnfonelemrn  12412  qnnen  12424  unbendc  12447  setsfun0  12490  srngbased  12597  srngplusgd  12598  srngmulrd  12599  srnginvld  12600  lmodbased  12615  lmodplusgd  12616  lmodscad  12617  lmodvscad  12618  ipsbased  12627  ipsaddgd  12628  ipsmulrd  12629  ipsscad  12630  ipsvscad  12631  ipsipd  12632  isnsgrp  12744  ismnd  12752  dfgrp2e  12835  subgintm  12989  srgisid  13100  srg1zr  13101  oppr1g  13183  dvdsr02  13205  isunitd  13206  crngunit  13211  unitpropdg  13248  subrguss  13295  subrgunit  13298  subrgugrp  13299  subrgintm  13302  tgval  13420  cldval  13470  ntrfval  13471  clsfval  13472  neifval  13511  neif  13512  neival  13514  cnclima  13594  cncnpi  13599  cnrest2  13607  cnrest2r  13608  cnptoprest  13610  cnpdis  13613  txvalex  13625  txval  13626  txcnmpt  13644  txdis  13648  cnmpt1t  13656  cnmpt2t  13664  hmeocnv  13678  hmeontr  13684  txhmeo  13690  xmetunirn  13729  xmettpos  13741  metn0  13749  xmetres  13753  metres  13754  blrnps  13782  blrn  13783  blin2  13803  blbas  13804  xmeterval  13806  xmettxlem  13880  xmettx  13881  metcnpi  13886  reldvg  14019  dvaddxx  14038  dvmulxx  14039  dviaddf  14040  dvimulf  14041  dvfre  14045  dveflem  14058  sinq12gt0  14122  rprelogbdiv  14246  logbgcd1irr  14256  lgslem4  14275  lgsdirprm  14306  bj-inex  14519  bj-sucexg  14534  bj-peano4  14567  setindis  14579  bdsetindis  14581  bj-inf2vnlem1  14582  nnsf  14614  nninfall  14618  nninfsellemeq  14623  sbthom  14634