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  1591  nfal  1622  19.9hd  1708  equsexd  1775  sbcof2  1856  aev  1858  sbequi  1885  nfsbd  2028  mo2n  2105  eupickb  2159  r19.29af2  2671  spc2gv  2895  spc3gv  2897  eqvincg  2928  sbcco3g  3183  ssrmof  3288  exmidsssnc  4291  exmid1stab  4296  snelpwi  4301  opth1  4326  frind  4447  onin  4481  abnexg  4541  reusv1  4553  xpexg  4838  reldmm  4948  dmexg  4994  rnexg  4995  elrelimasn  5100  relfld  5263  funimaexglem  5410  funimaexg  5411  fabexg  5521  fsnd  5624  elfvm  5668  nfvres  5671  funimass4  5692  elfvmptrab1  5737  funconstss  5761  f1oresrab  5808  resfunexg  5870  f1eqcocnv  5927  isores1  5950  isoini  5954  isose  5957  isopolem  5958  isosolem  5960  eusvobj2  5999  acexmidlemcase  6008  oprabid  6045  offval  6238  resfunexgALT  6265  offval3  6291  1stvalg  6300  2ndvalg  6301  1stcof  6321  2ndcof  6322  cnvf1o  6385  tposf12  6430  smores3  6454  smoiso  6463  tfr0dm  6483  tfrlemibxssdm  6488  tfrlemi14d  6494  tfrexlem  6495  tfr1onlemssrecs  6500  tfr1onlemsucfn  6501  tfr1onlemsucaccv  6502  tfr1onlembxssdm  6504  tfr1onlemres  6510  tfri1dALT  6512  tfrcllemssrecs  6513  tfrcllemsucfn  6514  tfrcllemsucaccv  6515  tfrcllembxssdm  6517  tfrcllemres  6523  rdgss  6544  nnsucsssuc  6655  nntr2  6666  swoord1  6726  swoord2  6727  iinerm  6771  eroveu  6790  pmresg  6840  en1uniel  6973  dom1o  6997  pw2f1odclem  7015  fopwdom  7017  xpen  7026  ssenen  7032  isinfinf  7081  ac6sfi  7082  preimaf1ofi  7144  sbthlem1  7150  fi0  7168  fiss  7170  supubti  7192  suplubti  7193  isotilem  7199  supisolem  7201  supisoex  7202  supisoti  7203  ordiso2  7228  eldju1st  7264  eldju2ndl  7265  updjud  7275  djudom  7286  ctmlemr  7301  enumctlemm  7307  nnnninfeq  7321  ctssexmid  7343  nninfwlpoimlemginf  7369  exmidonfinlem  7397  en2other2  7400  exmidaclem  7416  cc2lem  7478  cc3  7480  addclnq  7588  mulclnq  7589  1qec  7601  prarloclemarch2  7632  enq0tr  7647  addclnq0  7664  mulclnq0  7665  nq0m0r  7669  prarloclemlo  7707  prarloc  7716  genpml  7730  genpmu  7731  addnqprl  7742  addnqpru  7743  recnnpr  7761  prmuloc2  7780  1idpru  7804  ltexprlemm  7813  ltexprlemloc  7820  recexprlemm  7837  recexprlem1ssl  7846  caucvgprlemnkj  7879  caucvgprlemnbj  7880  caucvgprlemm  7881  caucvgprlemopl  7882  caucvgprlemlol  7883  caucvgprlemladdfu  7890  caucvgprlemladdrl  7891  caucvgprprlemk  7896  caucvgprprlemloccalc  7897  caucvgprprlemnkltj  7902  caucvgprprlemnjltk  7904  caucvgprprlemml  7907  caucvgprprlemmu  7908  caucvgprprlemlol  7911  caucvgprprlemexb  7920  caucvgprprlem1  7922  suplocexprlemml  7929  suplocexprlemlub  7937  addclsr  7966  mulclsr  7967  prsrcl  7997  caucvgsrlemoffcau  8011  peano5nnnn  8105  mulap0r  8788  nn1suc  9155  prime  9572  zindd  9591  xrlttri3  10025  xnn0xadd0  10095  fzopth  10289  fzsuc  10297  fzpred  10298  fzp1ss  10301  fztp  10306  fseq1p1m1  10322  1fv  10367  elfzom1elp1fzo  10440  ssfzo12  10462  fzosplitsn  10471  zsupcllemstep  10482  zsupcllemex  10483  infssuzledc  10487  divfl0  10549  fldiv4lem1div2uz2  10559  modqid  10604  modqmuladdim  10622  frecuzrdgtcl  10667  frecuzrdgfunlem  10674  frecfzennn  10681  frecfzen2  10682  seq3val  10715  seqvalcd  10716  seqsplitg  10744  iseqf1olemqcl  10754  iseqf1olemnab  10756  iseqf1olemmo  10760  iseqf1olemqk  10762  seq3f1olemstep  10769  seqf1oglem2  10775  seq3id3  10779  seqhomog  10785  faclbnd  10996  faclbnd3  10998  bcm1k  11015  hashfz1  11038  hashfz  11078  hashfzp1  11081  fiubm  11085  hashfacen  11093  leisorel  11094  wrdexb  11118  wrdsymb  11134  wrdred1hash  11150  lsw0  11154  lswex  11158  ccat0  11166  ccatval2  11168  ccatw2s1leng  11208  ccats1val2  11210  swrds1  11242  swrdlsw  11243  ccats1pfxeqrex  11289  pfxccatin12lem1  11302  swrdccatin2  11303  swrdccat  11309  cats1fvd  11340  cjcj  11437  caucvgre  11535  r19.2uz  11547  resqrexlemgt0  11574  ltabs  11641  xrmaxiflemab  11801  xrmaxiflemlub  11802  nnf1o  11930  summodclem2a  11935  fsumf1o  11944  fisum0diag2  12001  modfsummodlemstep  12011  fsumparts  12024  clim2prod  12093  prodfap0  12099  prodmodclem2a  12130  fprodssdc  12144  fprodcllem  12160  ef0lem  12214  resinval  12269  recosval  12270  demoivreALT  12328  nn0o  12461  gcdmultiplez  12585  dvdssq  12595  nninfct  12605  eucalg  12624  lcmgcdnn  12647  dvdsnprmd  12690  prm2orodd  12691  isprm5lem  12706  qnumdenbi  12757  nn0gcdsq  12765  phibnd  12782  hashdvds  12786  phimullem  12790  prmdiveq  12801  hashgcdlem  12803  modprm0  12820  nnnn0modprm0  12821  modprmn0modprm0  12822  oddprm  12825  prm23lt5  12829  pcprendvds  12856  pcidlem  12889  pcmpt  12909  pcfac  12916  infpnlem2  12926  prmunb  12928  1arith  12933  4sqlem19  12975  unennn  13011  ennnfonelemk  13014  ennnfonelemjn  13016  ennnfonelemhf1o  13027  ennnfonelemex  13028  ennnfonelemf1  13032  ennnfonelemrn  13033  qnnen  13045  unbendc  13068  setsfun0  13111  srngbased  13223  srngplusgd  13224  srngmulrd  13225  srnginvld  13226  lmodbased  13241  lmodplusgd  13242  lmodscad  13243  lmodvscad  13244  ipsbased  13253  ipsaddgd  13254  ipsmulrd  13255  ipsscad  13256  ipsvscad  13257  ipsipd  13258  tgval  13338  prdsbas3  13363  isnsgrp  13482  ismnd  13495  dfgrp2e  13604  subgintm  13778  eqg0el  13809  ecqusaddcl  13819  kerf1ghm  13854  gsumfzconst  13921  imasrng  13962  srgisid  13992  srg1zr  13993  qusring2  14072  oppr1g  14088  dvdsr02  14112  isunitd  14113  crngunit  14118  unitpropdg  14155  elrhmunit  14184  subrngintm  14219  subrguss  14243  subrgunit  14246  subrgugrp  14247  subrgintm  14250  lmodfopnelem1  14331  rmodislmodlem  14357  rmodislmod  14358  lssuni  14370  islss3  14386  lss0v  14437  sraval  14444  rnglidlmmgm  14503  2idllidld  14513  2idlridld  14514  rng2idl0  14526  rng2idlsubg0  14529  zrh0  14632  znle  14644  zndvds0  14657  znf1o  14658  znleval  14660  znfi  14662  znhash  14663  znunit  14666  psrbasg  14681  psradd  14686  psr0cl  14688  mpladd  14711  cldval  14816  ntrfval  14817  clsfval  14818  neifval  14857  neif  14858  neival  14860  cnclima  14940  cncnpi  14945  cnrest2  14953  cnrest2r  14954  cnptoprest  14956  cnpdis  14959  txvalex  14971  txval  14972  txcnmpt  14990  txdis  14994  cnmpt1t  15002  cnmpt2t  15010  hmeocnv  15024  hmeontr  15030  txhmeo  15036  xmetunirn  15075  xmettpos  15087  metn0  15095  xmetres  15099  metres  15100  blrnps  15128  blrn  15129  blin2  15149  blbas  15150  xmeterval  15152  xmettxlem  15226  xmettx  15227  metcnpi  15232  reldvg  15396  dvaddxx  15420  dvmulxx  15421  dviaddf  15422  dvimulf  15423  dvfre  15427  dvmptid  15433  dveflem  15443  elply2  15452  plyreres  15481  sinq12gt0  15547  rprelogbdiv  15674  logbgcd1irr  15684  fsumdvdsmul  15708  lgslem4  15725  lgsdirprm  15756  gausslemma2dlem0a  15771  gausslemma2dlem0f  15776  gausslemma2dlem0i  15779  gausslemma2dlem1a  15780  gausslemma2dlem1cl  15781  gausslemma2dlem5  15788  gausslemma2dlem6  15789  gausslemma2d  15791  lgseisenlem1  15792  lgseisenlem2  15793  lgseisenlem3  15794  lgseisen  15796  lgsquadlem1  15799  m1lgs  15807  2lgslem1a  15810  2lgslem1c  15812  2lgsoddprmlem2  15828  edgval  15904  edgstruct  15908  umgrnloopv  15958  umgredgprv  15959  upgr1edc  15965  umgredgne  15994  usgredgssen  16006  umgr2edg1  16053  uspgredg2vlem  16064  uspgr1edc  16084  wlkm  16150  wlkvtxiedg  16156  wlkvtxiedgg  16157  wlk1walkdom  16170  g0wlk0  16181  wlkres  16188  trlf1  16197  trlreslem  16198  trlres  16199  clwwlkg  16202  clwwlkccatlem  16209  clwwlknon  16238  eupthfi  16260  eupthseg  16261  eupthres  16266  bj-inex  16452  bj-sucexg  16467  bj-peano4  16500  setindis  16512  bdsetindis  16514  bj-inf2vnlem1  16515  nnsf  16557  nninfall  16561  nninfsellemeq  16566  sbthom  16580  gfsumval  16630