MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  anassrs Unicode version

Theorem anassrs 648
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
StepHypRef Expression
1 anassrs.1 . . 3
21exp32 605 . 2
32imp31 432 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  /\wa 369
This theorem is referenced by:  anass  649  mpanr1  683  pm2.61ddan  792  pm2.61dda  793  anass1rs  807  anabss5  816  anabss7  821  pm2.61da2ne  2776  ralimdvva  2868  2ralbida  2898  2ralbidva  2899  2rexbidva  2974  copsexg  4737  pofun  4821  imainss  5426  eqfnfv2  5982  fnex  6139  f1elima  6171  fliftfun  6210  isores2  6229  f1oiso  6247  ovmpt2dxf  6428  grpridd  6515  sorpssuni  6589  sorpssint  6590  tfindsg2  6696  oalim  7201  omlim  7202  oaass  7229  omlimcl  7246  omass  7248  oelim2  7263  oeoa  7265  oeoelem  7266  nnaass  7290  omabs  7315  eroveu  7425  sbthlem4  7650  fimaxg  7787  fisupg  7788  fofinf1o  7821  ordtypelem7  7970  hartogs  7990  card2on  8001  unwdomg  8031  wemapwe  8160  wemapweOLD  8161  dfac5  8530  cfsmolem  8671  isf32lem2  8755  ttukeylem6  8915  ondomon  8959  alephreg  8978  ltexprlem6  9440  recexsrlem  9501  wloglei  10110  recextlem2  10205  fimaxre  10515  creur  10555  uzind3OLD  10983  uz11  11132  xrmaxeq  11409  xrmineq  11410  xaddf  11452  xaddass  11470  xleadd1a  11474  xlt2add  11481  xmullem  11485  xmulgt0  11504  xmulasslem3  11507  xlemul1a  11509  xadddilem  11515  fzrevral  11792  seqcaopr2  12143  expnlbnd2  12297  faclbnd4lem4  12374  shftlem  12901  01sqrex  13083  cau3lem  13187  limsupbnd2  13306  clim2  13327  clim2c  13328  clim0c  13330  rlimresb  13388  2clim  13395  climabs0  13408  climcn1  13414  climcn2  13415  o1rlimmul  13441  climsqz  13463  climsqz2  13464  rlimsqzlem  13471  lo1le  13474  climsup  13492  caucvgrlem2  13497  iseralt  13507  summolem2  13538  fsum2dlem  13585  cvgcmp  13630  cvgcmpce  13632  climfsum  13634  fsumiun  13635  geomulcvg  13685  mertenslem2  13694  mertens  13695  prodfn0  13703  prodfrec  13704  zprod  13744  fprodeq0  13779  fprodn0  13783  fprod2dlem  13784  smu01lem  14135  gcdcllem1  14149  gcdmultiplez  14189  dvdssq  14198  coprmdvds2  14244  pclem  14362  pcge0  14385  pcgcd1  14400  prmpwdvds  14422  1arithlem4  14444  4sqlem18  14480  vdwlem10  14508  vdwlem11  14509  ramval  14526  ramub1lem2  14545  ramcl  14547  imasaddfnlem  14925  imasaddflem  14927  imasvscafn  14934  imasleval  14938  ismon2  15129  isepi2  15136  issubc3  15218  cofucl  15257  setcmon  15414  setcepi  15415  ipodrsfi  15793  ipodrsima  15795  isacs3lem  15796  grpidpropd  15888  gsumpropd2lem  15900  mhmpropd  15972  mhmima  15994  gsumccat  16009  grplcan  16102  mulgdirlem  16166  subgmulg  16215  issubg4  16220  subgint  16225  cycsubgcl  16227  ssnmz  16243  gastacl  16347  orbsta  16351  cntzsubg  16374  galactghm  16428  odmulg  16578  odbezout  16580  sylow3lem2  16648  lsmsubm  16673  efgsfo  16757  mulgmhm  16836  mulgghm  16837  gsumval3OLD  16908  gsumval3  16911  gsumcllem  16912  gsumcllemOLD  16913  gsumpt  16988  gsumptOLD  16989  gsum2d  16999  gsum2dOLD  17000  gsum2d2  17002  prdsgsum  17007  prdsgsumOLD  17008  subgdmdprd  17081  dprd2d2  17093  ablfac1eu  17124  srglmhm  17186  srgrmhm  17187  ringpropd  17230  ringlghm  17250  dvdsrpropd  17345  abvpropd  17491  islmodd  17518  lmodprop2d  17572  lsssubg  17603  lsspropd  17663  lmhmima  17693  lsmelval2  17731  lidlsubg  17862  assapropd  17976  asclpropd  17995  psrass1lem  18029  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  mplind  18167  evlslem2  18180  evlsval  18188  coe1tmmul2  18317  phlpropd  18690  frlmsslsp  18829  frlmsslspOLD  18830  lindfmm  18862  islindf4  18873  mamuass  18904  mavmulass  19051  mdetuni0  19123  mdetmul  19125  cpmatacl  19217  cpmadugsumfi  19378  cpmadugsum  19379  cpmadumatpolylem1  19382  cpmadumatpolylem2  19383  cpmadumatpoly  19384  cayhamlem4  19389  neips  19614  neindisj  19618  ordtrest2lem  19704  lmbrf  19761  lmss  19799  isreg2  19878  lmmo  19881  hauscmplem  19906  bwth  19910  2ndcomap  19959  1stcelcls  19962  restlly  19984  islly2  19985  cldllycmp  19996  comppfsc  20033  1stckgenlem  20054  txbas  20068  txbasval  20107  tx1cn  20110  ptpjopn  20113  ptcnp  20123  txnlly  20138  txlm  20149  xkococn  20161  fgabs  20380  fmfnfmlem4  20458  flimcf  20483  hauspwpwf1  20488  fclsbas  20522  fclscf  20526  flimfnfcls  20529  ghmcnp  20613  tsmsxp  20657  isxmet2d  20830  elmopn2  20948  mopni3  20997  blsscls2  21007  metequiv2  21013  metss2lem  21014  met2ndci  21025  metrest  21027  metcnp  21044  metcnp2  21045  metcnpi3  21049  txmetcnp  21050  nmolb2d  21225  xrge0tsms  21339  metdsre  21357  metnrmlem3  21365  fsumcn  21374  elcncf2  21394  mulc1cncf  21409  cncfco  21411  cncfmet  21412  bndth  21458  evth  21459  copco  21518  pcopt2  21523  pcoass  21524  pcorevlem  21526  lmmcvg  21700  lmmbrf  21701  iscau4  21718  iscauf  21719  cmetcaulem  21727  iscmet3lem3  21729  iscmet3lem1  21730  causs  21737  equivcfil  21738  lmclim  21741  caubl  21746  caublcls  21747  bcth3  21770  ivthle  21868  ivthle2  21869  ovoliunlem1  21913  ovolicc2lem5  21932  volsuplem  21965  uniioombllem6  21997  dyaddisjlem  22004  dyadmax  22007  volcn  22015  mbfmulc2lem  22054  ismbf3d  22061  mbfsup  22071  mbfinf  22072  mbflim  22075  i1fmullem  22101  itg2seq  22149  itg2uba  22150  itg2splitlem  22155  itg2split  22156  itg2monolem1  22157  ditgsplitlem  22264  ellimc2  22281  ellimc3  22283  limcflf  22285  limcmpt  22287  limcco  22297  lhop1lem  22414  dvfsumle  22422  dvfsumabs  22424  dvfsumrlim  22432  ftc1a  22438  ftc1lem6  22442  mdegmullem  22478  elply2  22593  plypf1  22609  ulmcaulem  22789  ulmcau  22790  ulmss  22792  ulmdvlem3  22797  mtest  22799  itgulm  22803  abelthlem8  22834  abelth  22836  tanord  22925  cxpcn3lem  23121  mcubic  23178  cubic2  23179  dvdsflsumcom  23464  fsumdvdsmul  23471  lgsdchrval  23622  2sqlem9  23648  rplogsumlem2  23670  rpvmasumlem  23672  dchrvmasumlem1  23680  vmalogdivsum2  23723  logsqvma  23727  selberg  23733  selberg4  23746  pntibndlem3  23777  pntlem3  23794  pntleml  23796  padicabv  23815  padicabvf  23816  padicabvcxp  23817  ostth3  23823  axpasch  24244  axcontlem7  24273  axcontlem10  24276  cusgrasize2inds  24477  2spotdisj  25061  grpolcan  25235  isgrp2d  25237  ghgrpOLD  25370  nvmul0or  25547  sspival  25651  nmosetre  25679  blocnilem  25719  blocni  25720  h2hcau  25896  h2hlm  25897  shsel3  26233  chscllem2  26556  homulcl  26678  adjsym  26752  cnvadj  26811  hhcno  26823  hhcnf  26824  lnopl  26833  unoplin  26839  counop  26840  lnfnl  26850  hmoplin  26861  hmopm  26940  nmcexi  26945  lnconi  26952  riesz3i  26981  leopmuli  27052  leopmul  27053  hstle  27149  mdsl0  27229  mdslmd1lem2  27245  atcvatlem  27304  chirredi  27313  cdj1i  27352  foresf1o  27403  isoun  27520  difioo  27593  xrge0tsmsd  27775  pstmxmet  27876  ordtrest2NEWlem  27904  dya2icoseg2  28249  eulerpartlemgc  28301  eulerpartlemgvv  28315  eulerpartlemgh  28317  eulerpartlemgs2  28319  ballotlemimin  28444  signstfvneq0  28529  conpcon  28680  cvmliftmolem2  28727  cvmliftlem6  28735  cvmliftlem8  28737  cvmlift2lem10  28757  cvmlift2lem12  28759  elmrsubrn  28880  relexpsucl  29055  relexpcnv  29056  relexpdm  29058  relexprn  29059  relexpadd  29061  relexpindlem  29062  rtrclreclem.trans  29069  rtrclreclem.min  29070  rtrclind  29072  dfon2lem6  29220  poseq  29333  nocvxminlem  29450  nofulllem5  29466  ifscgr  29694  brsegle  29758  finixpnum  30038  fin2solem  30039  fin2so  30040  heicant  30049  itg2gt0cn  30070  bddiblnc  30085  ftc1cnnc  30089  ftc1anclem5  30094  ftc1anclem6  30095  ftc1anclem7  30096  ftc1anc  30098  neibastop2lem  30178  cover2  30204  filbcmb  30231  fdc  30238  fdc1  30239  seqpo  30240  incsequz  30241  incsequz2  30242  metf1o  30248  lmclim2  30251  geomcau  30252  isbnd2  30279  bndss  30282  ismtybndlem  30302  heibor1lem  30305  rrncmslem  30328  rrnequiv  30331  exidreslem  30339  ghomco  30345  isdrngo3  30362  rngoisocnv  30384  isidlc  30412  idlnegcl  30419  divrngidl  30425  intidl  30426  unichnidl  30428  keridl  30429  igenmin  30461  prnc  30464  ispridlc  30467  prter3  30623  lsmfgcl  31020  kercvrlsm  31029  unxpwdom3  31041  hbt  31079  cntzsdrg  31151  cvgdvgrat  31194  lcmgcdlem  31212  lcmdvds  31214  climinf  31612  clim2f  31642  clim2cf  31656  clim0cf  31660  mgmhmpropd  32473  mgmhmima  32490  ovmpt2rdxf  32928  cotsqcscsq  33156  aacllem  33216  glbconxN  35102  atltcvr  35159  3dim1  35191  lvolnle3at  35306  linepsubN  35476  osumclN  35691  pexmidALTN  35702  lhpmatb  35755  cdlemg1idlemN  36298  dihlss  36977  dihglblem5aN  37019  dihatlat  37061
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 185  df-an 371
  Copyright terms: Public domain W3C validator