Theorem anassrs 469

Description: Associative law for conjunction applied to antecedent (eliminates syllogism). (Contributed by NM, 15-Nov-2002.)

Hypothesis

Ref	Expression
anassrs.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
anassrs	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem anassrs

Step	Hyp	Ref	Expression
1		anassrs.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 422	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 419	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  anass  470  anass1rs  654  anabss5  667  anabss7  672  mpanr1  702  pm2.61ddan  813  pm2.61dda  814  pm2.61da2ne  3031  ralimdvva  3205  reximdvva  3206  2ralbidva  3217  2rexbidva  3218  2ralbida  3281  copsexgw  5491  copsexg  5492  pofun  5607  imainss  6154  fvmptdf  7005  eqfnfv2  7034  fnex  7219  f1elima  7262  fliftfun  7309  isores2  7330  f1oiso  7348  ovmpodxf  7558  sorpssuni  7722  sorpssint  7723  tfindsg2  7851  2ndconst  8087  poxp2  8129  sexp3  8139  poseq  8144  oalim  8532  omlim  8533  oaass  8561  omlimcl  8578  omass  8580  oelim2  8595  oeoa  8597  oeoelem  8598  nnaass  8622  omabs  8650  eroveu  8806  sbthlem4  9086  fimaxg  9290  fisupg  9291  fofinf1o  9327  fiming  9493  fiinfg  9494  ordtypelem7  9519  hartogs  9539  card2on  9549  unwdomg  9579  wemapwe  9692  frmin  9744  dfac5  10123  cfsmolem  10265  isf32lem2  10349  ttukeylem6  10509  ondomon  10558  alephreg  10577  ltexprlem6  11036  recexsrlem  11098  wloglei  11746  recextlem2  11845  fimaxre  12158  creur  12206  uz11  12847  xrmaxeq  13158  xrmineq  13159  xaddf  13203  xaddass  13228  xleadd1a  13232  xlt2add  13239  xmullem  13243  xmulgt0  13262  xmulasslem3  13265  xlemul1a  13267  xadddilem  13273  fzrevral  13586  seqcaopr2  14004  expnlbnd2  14197  faclbnd4lem4  14256  hashgt23el  14384  rtrclreclem3  15007  rtrclreclem4  15008  relexpindlem  15010  rtrclind  15012  shftlem  15015  01sqrex  15196  cau3lem  15301  limsupbnd2  15427  clim2  15448  clim2c  15449  clim0c  15451  rlimresb  15509  2clim  15516  climabs0  15529  climcn1  15536  climcn2  15537  o1rlimmul  15563  climsqz  15585  climsqz2  15586  rlimsqzlem  15595  lo1le  15598  climsup  15616  caucvgrlem2  15621  iseralt  15631  summolem2  15662  fsum2dlem  15716  cvgcmp  15762  cvgcmpce  15764  climfsum  15766  fsumiun  15767  geomulcvg  15822  mertenslem2  15831  mertens  15832  prodfn0  15840  prodfrec  15841  zprod  15881  fprodeq0  15919  fprodn0  15923  fprod2dlem  15924  smu01lem  16426  gcdcllem1  16440  dvdssq  16504  lcmdvds  16545  coprmdvds2  16591  pclem  16771  pcge0  16795  pcgcd1  16810  prmpwdvds  16837  1arithlem4  16859  4sqlem18  16895  vdwlem10  16923  vdwlem11  16924  ramval  16941  ramub1lem2  16960  ramcl  16962  imasaddfnlem  17474  imasaddflem  17476  imasvscafn  17483  imasleval  17487  ismon2  17681  isepi2  17688  issubc3  17799  cofucl  17838  setcmon  18037  setcepi  18038  ipodrsfi  18492  ipodrsima  18494  isacs3lem  18495  grpidpropd  18581  grprida  18594  gsumpropd2lem  18598  mhmpropd  18678  mhmimalem  18705  grplcan  18885  dfgrp3lem  18921  mulgdirlem  18985  subgmulg  19020  issubg4  19025  subgint  19030  ssnmz  19046  cycsubgcl  19083  gastacl  19173  orbsta  19177  cntzsubg  19203  galactghm  19272  odmulg  19424  odbezout  19426  sylow3lem2  19496  lsmsubm  19521  efgsfo  19607  mulgmhm  19695  mulgghm  19696  gsumval3  19775  gsumcllem  19776  gsumpt  19830  gsum2d  19840  gsum2d2  19842  prdsgsum  19849  subgdmdprd  19904  dprd2d2  19914  ablfac1eu  19943  srglmhm  20044  srgrmhm  20045  ringpropd  20102  ringlghm  20124  dvdsrpropd  20230  cntzsdrg  20418  abvpropd  20450  islmodd  20477  lmodprop2d  20534  lsssubg  20568  lsspropd  20628  lmhmima  20658  lidlsubg  20838  phlpropd  21208  frlmsslsp  21351  lindfmm  21382  islindf4  21393  assapropd  21426  asclpropd  21451  psrass1lemOLD  21493  psrass1lem  21496  mplcoe1  21592  mplcoe5  21595  mplind  21631  evlslem2  21642  evlsval  21649  coe1tmmul2  21798  mamuass  21902  mavmulass  22051  mdetuni0  22123  mdetmul  22125  cpmatacl  22218  cpmadugsumfi  22379  cpmadumatpolylem1  22383  cpmadumatpolylem2  22384  cpmadumatpoly  22385  cayhamlem4  22390  neips  22617  neindisj  22621  ordtrest2lem  22707  lmbrf  22764  lmss  22802  isreg2  22881  lmmo  22884  hauscmplem  22910  bwth  22914  2ndcomap  22962  1stcelcls  22965  restlly  22987  islly2  22988  cldllycmp  22999  comppfsc  23036  1stckgenlem  23057  txbas  23071  txbasval  23110  tx1cn  23113  ptpjopn  23116  ptcnp  23126  txnlly  23141  txlm  23152  xkococn  23164  fgabs  23383  fmfnfmlem4  23461  flimcf  23486  hauspwpwf1  23491  fclsbas  23525  fclscf  23529  flimfnfcls  23532  ghmcnp  23619  tsmsxp  23659  isxmet2d  23833  elmopn2  23951  mopni3  24003  blsscls2  24013  metequiv2  24019  metss2lem  24020  met2ndci  24031  metrest  24033  metcnp  24050  metcnp2  24051  metcnpi3  24055  txmetcnp  24056  nmolb2d  24235  xrge0tsms  24350  metdsre  24369  metnrmlem3  24377  fsumcn  24386  elcncf2  24406  mulc1cncf  24421  cncfco  24423  cncfmet  24425  bndth  24474  evth  24475  copco  24534  pcopt2  24539  pcoass  24540  pcorevlem  24542  lmmcvg  24778  lmmbrf  24779  iscau4  24796  iscauf  24797  cmetcaulem  24805  iscmet3lem3  24807  iscmet3lem1  24808  causs  24815  equivcfil  24816  lmclim  24820  caubl  24825  caublcls  24826  bcth3  24848  ivthle  24973  ivthle2  24974  ovoliunlem1  25019  ovolicc2lem5  25038  volsuplem  25072  uniioombllem6  25105  dyaddisjlem  25112  dyadmax  25115  volcn  25123  mbfmulc2lem  25164  ismbf3d  25171  mbfsup  25181  mbfinf  25182  mbflim  25185  i1fmullem  25211  itg2seq  25260  itg2uba  25261  itg2splitlem  25266  itg2split  25267  itg2monolem1  25268  bddiblnc  25359  ditgsplitlem  25377  ellimc2  25394  ellimc3  25396  limcflf  25398  limcmpt  25400  limcco  25410  lhop1lem  25530  dvfsumle  25538  dvfsumabs  25540  dvfsumrlim  25548  ftc1a  25554  ftc1lem6  25558  mdegmullem  25596  elply2  25710  plypf1  25726  ulmcaulem  25906  ulmcau  25907  ulmss  25909  ulmdvlem3  25914  mtest  25916  itgulm  25920  abelthlem8  25951  abelth  25953  tanord  26047  cxpcn3lem  26255  mcubic  26352  cubic2  26353  dvdsflsumcom  26692  fsumdvdsmul  26699  lgsdchrval  26857  2sqlem9  26930  rplogsumlem2  26988  rpvmasumlem  26990  dchrvmasumlem1  26998  vmalogdivsum2  27041  logsqvma  27045  selberg  27051  selberg4  27064  pntibndlem3  27095  pntlem3  27112  pntleml  27114  padicabv  27133  padicabvf  27134  padicabvcxp  27135  ostth3  27141  nosupbnd1lem5  27215  noinfbnd1lem5  27230  nocvxminlem  27279  lrrecfr  27427  addsprop  27460  mulsproplem9  27580  mulsproplem12  27583  mulsproplem13  27584  mulsproplem14  27585  mulsprop  27586  slemuld  27594  mulsuniflem  27604  mulsasslem3  27620  axpasch  28199  axcontlem7  28228  axcontlem10  28231  cusgrsize2inds  28710  grpolcan  29783  nvmul0or  29903  nmosetre  30017  blocnilem  30057  blocni  30058  h2hcau  30232  h2hlm  30233  shsel3  30568  chscllem2  30891  homulcl  31012  adjsym  31086  cnvadj  31145  hhcno  31157  hhcnf  31158  lnopl  31167  unoplin  31173  counop  31174  lnfnl  31184  hmoplin  31195  hmopm  31274  nmcexi  31279  lnconi  31286  riesz3i  31315  leopmuli  31386  leopmul  31387  hstle  31483  mdsl0  31563  mdslmd1lem2  31579  atcvatlem  31638  chirredi  31647  cdj1i  31686  sbc2iedf  31707  foresf1o  31742  suppovss  31906  isoun  31923  difioo  31993  swrdf1  32120  xrge0tsmsd  32209  cycpmrn  32302  ressply1invg  32658  fedgmullem2  32715  pstmxmet  32877  ordtrest2NEWlem  32902  esum2dlem  33090  esum2d  33091  dya2icoseg2  33277  eulerpartlemgc  33361  eulerpartlemgh  33377  eulerpartlemgs2  33379  ballotlemimin  33504  signstfvneq0  33583  hgt750lemb  33668  connpconn  34226  cvmliftmolem2  34273  cvmliftlem6  34281  cvmliftlem8  34283  cvmlift2lem12  34305  elmrsubrn  34511  dfon2lem6  34760  ifscgr  35016  brsegle  35080  gg-dvfsumle  35182  neibastop2lem  35245  bj-elabd2ALT  35805  bj-ismooredr2  35991  curf  36466  finixpnum  36473  fin2solem  36474  fin2so  36475  lindsenlbs  36483  matunitlindflem1  36484  matunitlindflem2  36485  matunitlindf  36486  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem14  36502  poimirlem16  36504  poimirlem19  36507  poimirlem22  36510  poimirlem28  36516  poimirlem29  36517  poimirlem30  36518  poimir  36521  heicant  36523  itg2gt0cn  36543  ftc1cnnc  36560  ftc1anclem5  36565  ftc1anclem6  36566  ftc1anclem7  36567  ftc1anc  36569  cover2  36583  filbcmb  36608  fdc  36613  fdc1  36614  seqpo  36615  incsequz  36616  incsequz2  36617  metf1o  36623  lmclim2  36626  geomcau  36627  isbnd2  36651  bndss  36654  ismtybndlem  36674  heibor1lem  36677  rrncmslem  36700  rrnequiv  36703  exidreslem  36745  ghomco  36759  isdrngo3  36827  rngoisocnv  36849  isidlc  36883  idlnegcl  36890  divrngidl  36896  intidl  36897  unichnidl  36899  keridl  36900  igenmin  36932  prnc  36935  ispridlc  36938  erimeq2  37548  prter3  37752  glbconxN  38249  atltcvr  38306  3dim1  38338  lvolnle3at  38453  linepsubN  38623  osumclN  38838  pexmidALTN  38849  lhpmatb  38902  cdlemg1idlemN  39443  dihlss  40121  dihglblem5aN  40163  dihatlat  40205  metakunt1  40985  metakunt2  40986  f1o2d2  41055  pwsgprod  41114  selvvvval  41157  fsuppind  41162  fsuppssindlem1  41163  prjspertr  41347  prjspreln0  41351  lsmfgcl  41816  kercvrlsm  41825  unxpwdom3  41837  hbt  41872  oa0suclim  42025  om0suclim  42026  oe0suclim  42027  naddcnff  42112  cvgdvgrat  43072  climinf  44322  clim2f  44352  clim2cf  44366  clim0cf  44370  clim2f2  44386  fmtnofac2lem  46236  isomuspgrlem2d  46499  mgmhmpropd  46555  mgmhmima  46572  rngpropd  46673  rhmimasubrnglem  46744  ovmpordxf  47014  cotsqcscsq  47807  aacllem  47848