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

Theorem anass 649
Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 21-Jun-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)
Assertion
Ref Expression
anass

Proof of Theorem anass
StepHypRef Expression
1 id 22 . . 3
21anassrs 648 . 2
3 id 22 . . 3
43anasss 647 . 2
52, 4impbii 188 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369
This theorem is referenced by:  an12  797  an32  798  an13  799  an31  800  an4  824  3anass  977  3an4anass  1219  2sb5  2187  r2exfOLD  2979  r19.41v  3009  r19.41  3010  ceqsex3v  3149  ceqsrex2v  3235  rexrab  3263  rexrab2  3267  2reu5  3308  rexss  3566  inass  3707  indifdir  3753  difin2  3759  difrab  3771  reupick3  3782  inssdif0  3895  rexdifsn  4159  reusv2lem4  4656  reusv2  4658  eqvinop  4736  copsexg  4737  copsexgOLD  4738  wefrc  4878  rabxp  5041  elvvv  5064  resopab2  5327  difxp  5436  ssrnres  5450  cnvresima  5501  mptpreima  5505  coass  5531  imadif  5668  dff1o2  5826  eqfnfv3  5983  rexsuppOLD  6012  isoini  6234  f1oiso  6247  oprabid  6323  dfoprab2  6343  mpt2eq123  6356  mpt2mptx  6393  resoprab2  6399  ov3  6439  uniuni  6609  elxp4  6744  elxp5  6745  oprabex3  6789  frxp  6910  rexsupp  6937  brtpos2  6980  oeeui  7270  oeeu  7271  omabs  7315  mapsnen  7613  xpsnen  7621  xpcomco  7627  xpassen  7631  wemapsolem  7996  epfrs  8183  bnd2  8332  aceq1  8519  dfac5lem1  8525  dfac5lem2  8526  dfac5lem5  8529  kmlem3  8553  kmlem14  8564  pwfseqlem1  9057  ltexpi  9301  ltexprlem4  9438  axaddf  9543  axmulf  9544  rexuz  11160  rexuz2  11161  nnwos  11178  zmin  11207  rexrp  11268  elixx3g  11571  elfz2  11708  fzind2  11924  hashbclem  12501  resqrex  13084  rlim  13318  divalglem10  14060  divalgb  14062  gcdass  14183  isprm2  14225  infpn2  14431  ispos2  15577  issubg3  16219  resscntz  16369  subgdmdprd  17081  dprd2d2  17093  dfrhm2  17366  isassa  17964  aspval2  17996  fvmptnn04if  19350  istps2OLD  19422  istps3OLD  19423  ntreq0  19578  cmpcov2  19890  llyi  19975  nllyi  19976  subislly  19982  ptpjpre1  20072  tx1cn  20110  tx2cn  20111  txtube  20141  txkgen  20153  trfil2  20388  elflim2  20465  cnpflfi  20500  isfcls  20510  cnextcn  20567  istlm  20687  blres  20934  metrest  21027  isnlm  21184  elcncf1di  21399  elpi1  21545  iscph  21617  cfilucfil3OLD  21757  cfilucfil3  21758  itg1climres  22121  itgsubst  22450  ulmdvlem3  22797  cubic  23180  vmasum  23491  logfac2  23492  lgsquadlem1  23629  lgsquadlem2  23630  legov  23972  ltgov  23983  perpln1  24087  axcontlem5  24271  nb3grapr2  24454  trls  24538  3v3e3cycl2  24664  wwlknprop  24686  wwlkextwrd  24728  wwlknfi  24738  wlknwwlknvbij  24740  isclwlk  24756  clwwlkvbij  24801  usg2spthonot0  24889  usg2spthonot1  24890  rusgranumwlkl1  24947  rusgranumwlklem3  24951  rusgra0edg  24955  1to2vfriswmgra  25006  usgreg2spot  25067  numclwwlkovf2  25084  grpoidinvlem3  25208  h2hlm  25897  issh  26125  issh3  26137  ocsh  26201  cvbr2  27202  cvnbtwn2  27206  mdsl2i  27241  cvmdi  27243  mdsymlem2  27323  sumdmdii  27334  spc2ed  27372  rabrab  27399  disjunsn  27453  mpt2mptxf  27518  1stpreima  27524  2ndpreima  27525  f1od2  27547  nndiffz1  27596  omndmul2  27702  crefdf  27851  pcmplfin  27863  1stmbfm  28231  2ndmbfm  28232  dya2iocnei  28253  eulerpartlemgvv  28315  eulerpartlemn  28320  iscvm  28704  axacprim  29079  dfpo2  29184  dfdm5  29206  dfrn5  29207  elima4  29209  preduz  29280  wfi  29287  frind  29323  sltval2  29416  nofulllem5  29466  dfon3  29542  brimg  29587  brsuccf  29591  dfrdg4  29600  tfrqfree  29601  ifscgr  29694  cgrxfr  29705  segcon2  29755  seglecgr12im  29760  segletr  29764  ellines  29802  itg2addnc  30069  ftc1anclem5  30094  ftc1anc  30098  areacirclem5  30111  neifg  30189  isbnd2  30279  heibor1  30306  mergeconj  30502  prtlem70  30592  prtlem100  30596  diophrex  30709  rmxdioph  30958  dford4  30971  islmodfg  31015  islssfg2  31017  isdomn3  31164  fgraphopab  31170  lcmass  31218  2sbc5g  31323  limcrecl  31635  dvnmul  31740  dvnprodlem2  31744  fourierdlem83  31972  rexdifpr  32300  usgra2pth0  32355  isrnghm  32698  isrnghmmul  32699  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  mpt2mptx2  32924  bnj250  33753  bnj251  33754  bnj256  33758  bnj168  33785  lsateln0  34720  islshpat  34742  lcvbr2  34747  lcvnbtwn2  34752  isopos  34905  cvrval2  34999  cvrnbtwn2  35000  ishlat2  35078  3dim0  35181  islvol5  35303  pmapjat1  35577  pclcmpatN  35625  pclfinclN  35674  cdlemefrs29pre00  36121  cdlemefrs29bpre0  36122  cdlemefrs29cpre1  36124  cdleme32a  36167  cdlemftr3  36291  dvhopellsm  36844  dibelval3  36874  diblsmopel  36898  mapdvalc  37356  mapdval4N  37359  mapdordlem1a  37361
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