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 ⊢ (𝜑 → 𝜃)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7

This theorem is used by:  4syl  18  simpl2im  390  hbim  1598  nfal  1629  19.9hd  1714  equsexd  1782  sbcof2  1863  aev  1865  sbequi  1892  nfsbd  2037  mo2n  2114  eupickb  2168  r19.29af2  2691  spc2gv  2916  spc3gv  2918  eqvincg  2950  sbcco3g  3205  ssrmof  3311  exmidsssnc  4340  exmid1stab  4345  snelpwi  4351  opth1  4376  frind  4497  onin  4531  abnexg  4592  reusv1  4604  xpexg  4889  reldmm  5000  dmexg  5046  rnexg  5047  elrelimasn  5153  relfld  5316  funimaexglem  5464  funimaexg  5465  fabexg  5579  fsnd  5684  elfvm  5729  nfvres  5732  funimass4  5753  elfvmptrab1  5801  funconstss  5827  f1oresrab  5873  resfunexg  5936  f1eqcocnv  5997  isores1  6020  isoini  6024  isose  6027  isopolem  6028  isosolem  6030  eusvobj2  6071  acexmidlemcase  6080  oprabid  6117  offval  6310  resfunexgALT  6337  offval3  6367  1stvalg  6376  2ndvalg  6377  1stcof  6397  2ndcof  6398  cnvf1o  6461  tposf12  6540  smores3  6564  smoiso  6573  tfr0dm  6593  tfrlemibxssdm  6598  tfrlemi14d  6604  tfrexlem  6605  tfr1onlemssrecs  6610  tfr1onlemsucfn  6611  tfr1onlemsucaccv  6612  tfr1onlembxssdm  6614  tfr1onlemres  6620  tfri1dALT  6622  tfrcllemssrecs  6623  tfrcllemsucfn  6624  tfrcllemsucaccv  6625  tfrcllembxssdm  6627  tfrcllemres  6633  rdgss  6654  nnsucsssuc  6765  nntr2  6776  swoord1  6836  swoord2  6837  iinerm  6881  eroveu  6900  pmresg  6957  en1uniel  7091  dom1o  7116  pw2f1odclem  7134  fopwdom  7136  xpen  7145  mapunen  7151  ssenen  7152  isinfinf  7201  ac6sfi  7202  preimaf1ofi  7268  sbthlem1  7274  fczfsuppd  7297  fi0  7309  fiss  7311  supubti  7340  suplubti  7341  isotilem  7347  supisolem  7349  supisoex  7350  supisoti  7351  ordiso2  7376  eldju1st  7412  eldju2ndl  7413  updjud  7423  djudom  7434  ctmlemr  7449  enumctlemm  7455  nnnninfeq  7469  ctssexmid  7491  nninfwlpoimlemginf  7517  exmidonfinlem  7546  en2other2  7549  exmidaclem  7565  cc2lem  7633  cc3  7635  addclnq  7743  mulclnq  7744  1qec  7756  prarloclemarch2  7787  enq0tr  7802  addclnq0  7819  mulclnq0  7820  nq0m0r  7824  prarloclemlo  7862  prarloc  7871  genpml  7885  genpmu  7886  addnqprl  7897  addnqpru  7898  recnnpr  7916  prmuloc2  7935  1idpru  7959  ltexprlemm  7968  ltexprlemloc  7975  recexprlemm  7992  recexprlem1ssl  8001  caucvgprlemnkj  8034  caucvgprlemnbj  8035  caucvgprlemm  8036  caucvgprlemopl  8037  caucvgprlemlol  8038  caucvgprlemladdfu  8045  caucvgprlemladdrl  8046  caucvgprprlemk  8051  caucvgprprlemloccalc  8052  caucvgprprlemnkltj  8057  caucvgprprlemnjltk  8059  caucvgprprlemml  8062  caucvgprprlemmu  8063  caucvgprprlemlol  8066  caucvgprprlemexb  8075  caucvgprprlem1  8077  suplocexprlemml  8084  suplocexprlemlub  8092  addclsr  8121  mulclsr  8122  prsrcl  8152  caucvgsrlemoffcau  8166  peano5nnnn  8260  mulap0r  8946  indv  9298  nn1suc  9326  prime  9750  zindd  9769  xrlttri3  10210  xnn0xadd0  10280  fzopth  10478  fzsuc  10486  fzpred  10488  fzp1ss  10491  fztp  10496  fseq1p1m1  10512  1fv  10557  elfzom1elp1fzo  10631  ssfzo12  10653  fzosplitsn  10662  zsupcllemstep  10673  zsupcllemex  10674  infssuzledc  10678  divfl0  10745  fldiv4lem1div2uz2  10755  modqid  10800  modqmuladdim  10818  frecuzrdgtcl  10863  frecuzrdgfunlem  10870  frecfzennn  10877  frecfzen2  10878  seq3val  10911  seqvalcd  10912  seqsplitg  10940  iseqf1olemqcl  10950  iseqf1olemnab  10952  iseqf1olemmo  10956  iseqf1olemqk  10958  seq3f1olemstep  10965  seqf1oglem2  10971  seq3id3  10975  seqhomog  10981  faclbnd  11194  faclbnd3  11196  bcm1k  11213  hashfz1  11237  hashfz  11277  hashfzp1  11280  fiubm  11286  hashfacen  11299  leisorel  11304  wrdexb  11331  wrdsymb  11347  wrdred1hash  11363  lsw0  11367  lswex  11371  ccat0  11379  ccatval2  11381  ccatw2s1leng  11421  ccats1val2  11423  swrds1  11455  swrdlsw  11456  ccats1pfxeqrex  11502  pfxccatin12lem1  11515  swrdccatin2  11516  swrdccat  11522  cats1fvd  11553  s1s2d  11581  s1s3d  11582  cjcj  11663  caucvgre  11762  r19.2uz  11774  resqrexlemgt0  11801  ltabs  11869  xrmaxiflemab  12031  xrmaxiflemlub  12032  nnf1o  12161  summodclem2a  12166  fsumf1o  12175  fisum0diag2  12232  modfsummodlemstep  12242  fsumparts  12255  clim2prod  12324  prodfap0  12330  prodmodclem2a  12361  fprodssdc  12375  fprodcllem  12391  ef0lem  12445  resinval  12500  recosval  12501  demoivreALT  12559  nn0o  12692  gcdmultiplez  12816  dvdssq  12826  nninfct  12836  eucalg  12855  lcmgcdnn  12878  dvdsnprmd  12921  prm2orodd  12922  isprm5lem  12938  qnumdenbi  12990  nn0gcdsq  12998  phibnd  13017  hashdvds  13021  phimullem  13025  prmdiveq  13036  hashgcdlem  13038  modprm0  13055  nnnn0modprm0  13056  modprmn0modprm0  13057  oddprm  13060  prm23lt5  13064  pcprendvds  13091  pcidlem  13124  pcmpt  13144  pcfac  13151  infpnlem2  13161  prmunb  13163  1arith  13168  4sqlem19  13210  ballotfilemfp1  13282  ballotfilemic  13301  ballotfilem1c  13302  ballotfilemsima  13310  ballotfilemrv  13314  ballotfilemro  13317  ballotfilemfrc  13321  ballotfilemfrci  13322  ballotfilemfrceq  13323  ballotfilemfrcn0  13324  ballotfilemrinv0  13327  unennn  13339  ennnfonelemk  13342  ennnfonelemjn  13344  ennnfonelemhf1o  13355  ennnfonelemex  13356  ennnfonelemf1  13360  ennnfonelemrn  13361  qnnen  13373  unbendc  13396  setsfun0  13439  srngbased  13552  srngplusgd  13553  srngmulrd  13554  srnginvld  13555  lmodbased  13570  lmodplusgd  13571  lmodscad  13572  lmodvscad  13573  ipsbased  13582  ipsaddgd  13583  ipsmulrd  13584  ipsscad  13585  ipsvscad  13586  ipsipd  13587  tgval  13667  gzsumval2  13765  isnsgrp  13772  ismnd  13783  dfgrp2e  13884  subgintm  14052  eqg0el  14083  ecqusaddcl  14093  kerf1ghm  14128  gzsumconst  14194  gsumvalfi  14203  gsumf1ofi  14211  prdsbas3  14238  imasrng  14306  srgisid  14341  qusring2  14422  oppr1g  14439  dvdsr02  14463  isunitd  14464  crngunit  14469  unitpropdg  14506  elrhmunit  14535  subrngintm  14571  subrguss  14595  subrgunit  14598  subrgugrp  14599  subrgintm  14602  drngunz  14669  lmodfopnelem1  14712  rmodislmodlem  14738  rmodislmod  14739  lssuni  14751  islss3  14767  lss0v  14818  sraval  14825  rnglidlmmgm  14884  2idllidld  14894  2idlridld  14895  rng2idl0  14907  rng2idlsubg0  14910  zrh0  15011  znle  15023  zndvds0  15036  znf1o  15037  znleval  15039  znfi  15041  znhash  15042  znunit  15045  issubassa  15064  asclfval  15072  ascl0  15078  ascl1  15079  rnasclsubrg  15087  psrbaglecl  15111  psrbasg  15117  psradd  15122  psr0cl  15124  mpladd  15147  cldval  15252  ntrfval  15253  clsfval  15254  neifval  15293  neif  15294  neival  15296  cnclima  15376  cncnpi  15381  cnrest2  15389  cnrest2r  15390  cnptoprest  15392  cnpdis  15395  txvalex  15407  txval  15408  txcnmpt  15426  txdis  15430  cnmpt1t  15438  cnmpt2t  15446  hmeocnv  15460  hmeontr  15466  txhmeo  15472  xmetunirn  15511  xmettpos  15523  metn0  15531  xmetres  15535  metres  15536  blrnps  15564  blrn  15565  blin2  15585  blbas  15586  xmeterval  15588  xmettxlem  15662  xmettx  15663  metcnpi  15668  reldvg  15832  dvaddxx  15856  dvmulxx  15857  dviaddf  15858  dvimulf  15859  dvfre  15863  dvmptid  15869  dveflem  15879  elply2  15888  plyreres  15917  sinq12gt0  15984  logfac  16051  rprelogbdiv  16115  logbgcd1irr  16125  birthdaylem3  16149  ppinprm  16182  chtnprm  16184  ppiqp1le  16189  fsumdvdsmul  16207  bcmono  16226  bposlem1  16233  bposlem3  16235  bposlem5  16237  lgslem4  16244  lgsdirprm  16275  gausslemma2dlem0a  16290  gausslemma2dlem0f  16295  gausslemma2dlem0i  16298  gausslemma2dlem1a  16299  gausslemma2dlem1cl  16300  gausslemma2dlem5  16307  gausslemma2dlem6  16308  gausslemma2d  16310  lgseisenlem1  16311  lgseisenlem2  16312  lgseisenlem3  16313  lgseisen  16315  lgsquadlem1  16318  m1lgs  16326  2lgslem1a  16329  2lgslem1c  16331  2lgsoddprmlem2  16347  edgval  16423  edgstruct  16427  umgrnloopv  16477  umgredgprv  16478  upgr1edc  16484  umgredgne  16513  usgredgssen  16525  umgr2edg1  16572  uspgredg2vlem  16583  uspgr1edc  16603  uhgrspansubgrlem  16639  wlkm  16702  wlkvtxiedg  16708  wlkvtxiedgg  16709  wlk1walkdom  16722  g0wlk0  16733  wlkres  16742  trlf1  16751  trlreslem  16752  trlres  16753  clwwlkg  16756  clwwlkccatlem  16763  clwwlknon  16792  eupthfi  16814  eupthseg  16815  eupthres  16820  trlsegvdeglem1  16823  trlsegvdeglem7  16829  trlsegvdegfi  16830  eupth2lem3lem2fi  16832  eupth2lem3lem3fi  16833  eupth2lem3lem6fi  16834  eupth2lem3lem4fi  16836  eupth2lem3lem7fi  16837  eupth2lem3fi  16839  eupth2lemsfi  16841  eupth2fi  16842  konigsbergssiedgwen  16849  bj-inex  17055  bj-sucexg  17070  bj-peano4  17103  setindis  17115  bdsetindis  17117  bj-inf2vnlem1  17118  wexmiddiffilem  17165  wexmiddifxy  17168  nnsf  17170  nninfall  17174  nninfsellemeq  17179  sbthom  17193