Theorem anassrs 471

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 424	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp31 421	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  anass  472  anass1rs  655  anabss5  668  anabss7  673  mpanr1  703  pm2.61ddan  814  pm2.61dda  815  pm2.61da2ne  3022  ralimdvva  3093  2ralbidva  3110  2ralbida  3146  reximdvva  3187  2rexbidva  3209  copsexgw  5347  copsexg  5348  pofun  5460  imainss  5986  fvmptdf  6783  eqfnfv2  6812  fnex  6992  f1elima  7034  fliftfun  7080  isores2  7101  f1oiso  7119  ovmpodxf  7317  sorpssuni  7478  sorpssint  7479  tfindsg2  7597  2ndconst  7824  oalim  8190  omlim  8191  oaass  8220  omlimcl  8237  omass  8239  oelim2  8254  oeoa  8256  oeoelem  8257  nnaass  8281  omabs  8307  eroveu  8425  sbthlem4  8682  fimaxg  8841  fisupg  8842  fofinf1o  8874  fiming  9037  fiinfg  9038  ordtypelem7  9063  hartogs  9083  card2on  9093  unwdomg  9123  wemapwe  9235  dfac5  9630  cfsmolem  9772  isf32lem2  9856  ttukeylem6  10016  ondomon  10065  alephreg  10084  ltexprlem6  10543  recexsrlem  10605  wloglei  11252  recextlem2  11351  fimaxre  11664  creur  11712  uz11  12351  xrmaxeq  12657  xrmineq  12658  xaddf  12702  xaddass  12727  xleadd1a  12731  xlt2add  12738  xmullem  12742  xmulgt0  12761  xmulasslem3  12764  xlemul1a  12766  xadddilem  12772  fzrevral  13085  seqcaopr2  13500  expnlbnd2  13689  faclbnd4lem4  13750  hashgt23el  13879  rtrclreclem3  14511  rtrclreclem4  14512  relexpindlem  14514  rtrclind  14516  shftlem  14519  01sqrex  14701  cau3lem  14806  limsupbnd2  14932  clim2  14953  clim2c  14954  clim0c  14956  rlimresb  15014  2clim  15021  climabs0  15034  climcn1  15041  climcn2  15042  o1rlimmul  15068  climsqz  15090  climsqz2  15091  rlimsqzlem  15100  lo1le  15103  climsup  15121  caucvgrlem2  15126  iseralt  15136  summolem2  15168  fsum2dlem  15220  cvgcmp  15266  cvgcmpce  15268  climfsum  15270  fsumiun  15271  geomulcvg  15326  mertenslem2  15335  mertens  15336  prodfn0  15344  prodfrec  15345  zprod  15385  fprodeq0  15423  fprodn0  15427  fprod2dlem  15428  smu01lem  15930  gcdcllem1  15944  gcdmultiplezOLD  15999  dvdssq  16010  lcmdvds  16051  coprmdvds2  16097  pclem  16277  pcge0  16300  pcgcd1  16315  prmpwdvds  16342  1arithlem4  16364  4sqlem18  16400  vdwlem10  16428  vdwlem11  16429  ramval  16446  ramub1lem2  16465  ramcl  16467  imasaddfnlem  16906  imasaddflem  16908  imasvscafn  16915  imasleval  16919  ismon2  17111  isepi2  17118  issubc3  17226  cofucl  17265  setcmon  17461  setcepi  17462  ipodrsfi  17891  ipodrsima  17893  isacs3lem  17894  grpidpropd  17990  grpridd  18003  gsumpropd2lem  18007  mhmpropd  18080  mhmima  18107  gsumccatOLD  18123  grplcan  18281  dfgrp3lem  18317  mulgdirlem  18378  subgmulg  18413  issubg4  18418  subgint  18423  ssnmz  18438  cycsubgcl  18469  gastacl  18559  orbsta  18563  cntzsubg  18587  galactghm  18652  odmulg  18803  odbezout  18805  sylow3lem2  18873  lsmsubm  18898  efgsfo  18985  mulgmhm  19069  mulgghm  19070  gsumval3  19148  gsumcllem  19149  gsumpt  19203  gsum2d  19213  gsum2d2  19215  prdsgsum  19222  subgdmdprd  19277  dprd2d2  19287  ablfac1eu  19316  srglmhm  19406  srgrmhm  19407  ringpropd  19456  ringlghm  19478  dvdsrpropd  19570  cntzsdrg  19702  abvpropd  19734  islmodd  19761  lmodprop2d  19817  lsssubg  19850  lsspropd  19910  lmhmima  19940  lidlsubg  20109  phlpropd  20473  frlmsslsp  20614  lindfmm  20645  islindf4  20656  assapropd  20687  asclpropd  20713  psrass1lemOLD  20755  psrass1lem  20758  mplcoe1  20850  mplcoe5  20853  mplind  20884  evlslem2  20895  evlsval  20902  coe1tmmul2  21053  mamuass  21155  mavmulass  21302  mdetuni0  21374  mdetmul  21376  cpmatacl  21469  cpmadugsumfi  21630  cpmadumatpolylem1  21634  cpmadumatpolylem2  21635  cpmadumatpoly  21636  cayhamlem4  21641  neips  21866  neindisj  21870  ordtrest2lem  21956  lmbrf  22013  lmss  22051  isreg2  22130  lmmo  22133  hauscmplem  22159  bwth  22163  2ndcomap  22211  1stcelcls  22214  restlly  22236  islly2  22237  cldllycmp  22248  comppfsc  22285  1stckgenlem  22306  txbas  22320  txbasval  22359  tx1cn  22362  ptpjopn  22365  ptcnp  22375  txnlly  22390  txlm  22401  xkococn  22413  fgabs  22632  fmfnfmlem4  22710  flimcf  22735  hauspwpwf1  22740  fclsbas  22774  fclscf  22778  flimfnfcls  22781  ghmcnp  22868  tsmsxp  22908  isxmet2d  23082  elmopn2  23200  mopni3  23249  blsscls2  23259  metequiv2  23265  metss2lem  23266  met2ndci  23277  metrest  23279  metcnp  23296  metcnp2  23297  metcnpi3  23301  txmetcnp  23302  nmolb2d  23473  xrge0tsms  23588  metdsre  23607  metnrmlem3  23615  fsumcn  23624  elcncf2  23644  mulc1cncf  23659  cncfco  23661  cncfmet  23663  bndth  23712  evth  23713  copco  23772  pcopt2  23777  pcoass  23778  pcorevlem  23780  lmmcvg  24015  lmmbrf  24016  iscau4  24033  iscauf  24034  cmetcaulem  24042  iscmet3lem3  24044  iscmet3lem1  24045  causs  24052  equivcfil  24053  lmclim  24057  caubl  24062  caublcls  24063  bcth3  24085  ivthle  24210  ivthle2  24211  ovoliunlem1  24256  ovolicc2lem5  24275  volsuplem  24309  uniioombllem6  24342  dyaddisjlem  24349  dyadmax  24352  volcn  24360  mbfmulc2lem  24401  ismbf3d  24408  mbfsup  24418  mbfinf  24419  mbflim  24422  i1fmullem  24448  itg2seq  24497  itg2uba  24498  itg2splitlem  24503  itg2split  24504  itg2monolem1  24505  bddiblnc  24596  ditgsplitlem  24614  ellimc2  24631  ellimc3  24633  limcflf  24635  limcmpt  24637  limcco  24647  lhop1lem  24767  dvfsumle  24775  dvfsumabs  24777  dvfsumrlim  24785  ftc1a  24791  ftc1lem6  24795  mdegmullem  24833  elply2  24947  plypf1  24963  ulmcaulem  25143  ulmcau  25144  ulmss  25146  ulmdvlem3  25151  mtest  25153  itgulm  25157  abelthlem8  25188  abelth  25190  tanord  25284  cxpcn3lem  25490  mcubic  25587  cubic2  25588  dvdsflsumcom  25927  fsumdvdsmul  25934  lgsdchrval  26092  2sqlem9  26165  rplogsumlem2  26223  rpvmasumlem  26225  dchrvmasumlem1  26233  vmalogdivsum2  26276  logsqvma  26280  selberg  26286  selberg4  26299  pntibndlem3  26330  pntlem3  26347  pntleml  26349  padicabv  26368  padicabvf  26369  padicabvcxp  26370  ostth3  26376  axpasch  26889  axcontlem7  26918  axcontlem10  26921  cusgrsize2inds  27397  grpolcan  28467  nvmul0or  28587  nmosetre  28701  blocnilem  28741  blocni  28742  h2hcau  28916  h2hlm  28917  shsel3  29252  chscllem2  29575  homulcl  29696  adjsym  29770  cnvadj  29829  hhcno  29841  hhcnf  29842  lnopl  29851  unoplin  29857  counop  29858  lnfnl  29868  hmoplin  29879  hmopm  29958  nmcexi  29963  lnconi  29970  riesz3i  29999  leopmuli  30070  leopmul  30071  hstle  30167  mdsl0  30247  mdslmd1lem2  30263  atcvatlem  30322  chirredi  30331  cdj1i  30370  sbc2iedf  30391  foresf1o  30426  suppovss  30594  isoun  30611  difioo  30680  swrdf1  30805  xrge0tsmsd  30896  cycpmrn  30989  fedgmullem2  31285  pstmxmet  31421  ordtrest2NEWlem  31446  esum2dlem  31632  esum2d  31633  dya2icoseg2  31817  eulerpartlemgc  31901  eulerpartlemgh  31917  eulerpartlemgs2  31919  ballotlemimin  32044  signstfvneq0  32123  hgt750lemb  32208  connpconn  32770  cvmliftmolem2  32817  cvmliftlem6  32825  cvmliftlem8  32827  cvmlift2lem12  32849  elmrsubrn  33055  dfon2lem6  33340  poxp2  33405  xpord3pred  33413  sexp3  33414  poseq  33417  nosupbnd1lem5  33560  noinfbnd1lem5  33575  nocvxminlem  33617  lrrecfr  33745  ifscgr  33991  brsegle  34055  neibastop2lem  34194  bj-ismooredr2  34924  curf  35400  finixpnum  35407  fin2solem  35408  fin2so  35409  lindsenlbs  35417  matunitlindflem1  35418  matunitlindflem2  35419  matunitlindf  35420  poimirlem3  35425  poimirlem4  35426  poimirlem6  35428  poimirlem7  35429  poimirlem14  35436  poimirlem16  35438  poimirlem19  35441  poimirlem22  35444  poimirlem28  35450  poimirlem29  35451  poimirlem30  35452  poimir  35455  heicant  35457  itg2gt0cn  35477  ftc1cnnc  35494  ftc1anclem5  35499  ftc1anclem6  35500  ftc1anclem7  35501  ftc1anc  35503  cover2  35517  filbcmb  35543  fdc  35548  fdc1  35549  seqpo  35550  incsequz  35551  incsequz2  35552  metf1o  35558  lmclim2  35561  geomcau  35562  isbnd2  35586  bndss  35589  ismtybndlem  35609  heibor1lem  35612  rrncmslem  35635  rrnequiv  35638  exidreslem  35680  ghomco  35694  isdrngo3  35762  rngoisocnv  35784  isidlc  35818  idlnegcl  35825  divrngidl  35831  intidl  35832  unichnidl  35834  keridl  35835  igenmin  35867  prnc  35870  ispridlc  35873  erim2  36434  prter3  36541  glbconxN  37037  atltcvr  37094  3dim1  37126  lvolnle3at  37241  linepsubN  37411  osumclN  37626  pexmidALTN  37637  lhpmatb  37690  cdlemg1idlemN  38231  dihlss  38909  dihglblem5aN  38951  dihatlat  38993  metakunt1  39738  metakunt2  39739  pwsgprod  39872  fsuppind  39880  fsuppssindlem1  39881  prjspertr  40043  prjspreln0  40047  lsmfgcl  40493  kercvrlsm  40502  unxpwdom3  40514  hbt  40549  cvgdvgrat  41491  climinf  42711  clim2f  42741  clim2cf  42755  clim0cf  42759  clim2f2  42775  fmtnofac2lem  44583  isomuspgrlem2d  44846  mgmhmpropd  44902  mgmhmima  44919  ovmpordxf  45237  cotsqcscsq  45946  aacllem  45987