Theorem anass 468

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

Step	Hyp	Ref	Expression
1		id 22	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
2	1	anassrs 467	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		id 22	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	anasss 466	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	2, 4	impbii 209	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  bianass  641  an31  647  an4  655  3anass  1095  3an4anass  1105  an33rean  1483  2sb5  2281  r19.41v  3195  r3ex  3204  r19.41  3269  rabrabi  3463  rabrab  3468  ceqsex3v  3549  spc2ed  3614  ceqsrex2v  3671  rexrab  3718  rexrab2  3722  reurab  3723  2reu5  3780  rexss  4084  inass  4249  rexin  4269  difin2  4320  difrab  4337  reupick3  4349  inssdif0  4397  rabsneq  4666  rexdifpr  4681  rexdifsn  4819  reusv2lem4  5419  reusv2  5421  eqvinop  5507  copsexgw  5510  copsexg  5511  rabxp  5748  elvvv  5775  resopab2  6065  difxp  6195  mptpreima  6269  resco  6281  coass  6296  dfpo2  6327  frpoind  6374  wfiOLD  6383  imadif  6662  dff1o2  6867  eqfnfv3  7066  f1ossf1o  7162  isoini  7374  f1oiso  7387  riotarab  7447  oprabidw  7479  oprabid  7480  dfoprab2  7508  mpoeq123  7522  mpomptx  7563  resoprab2  7569  ov3  7613  uniuni  7797  elxp4  7962  elxp5  7963  oprabex3  8018  frxp  8167  rexsupp  8223  brtpos2  8273  oeeui  8658  oeeu  8659  omabs  8707  eldifsucnn  8720  naddsuc2  8757  mapsnend  9101  xpsnen  9121  xpcomco  9128  xpassen  9132  wemapsolem  9619  epfrs  9800  frind  9819  aceq1  10186  dfac5lem1  10192  dfac5lem2  10193  dfac5lem5  10196  kmlem3  10222  kmlem14  10233  pwfseqlem1  10727  ltexpi  10971  ltexprlem4  11108  axaddf  11214  axmulf  11215  rexuz  12963  rexuz2  12964  nnwos  12980  zmin  13009  rexrp  13078  elixx3g  13420  elfz2  13574  preduz  13707  fzind2  13835  hashbclem  14501  resqrex  15299  rlim  15541  divalglem10  16450  divalgb  16452  gcdass  16594  lcmass  16661  isprm2  16729  infpn2  16960  ispos2  18385  issubmndb  18840  issubg3  19184  resscntz  19373  subgdmdprd  20078  dprd2d2  20088  isrnghm  20467  isrnghmmul  20468  dfrhm2  20500  rngcinv  20659  ringcinv  20693  isdomn3  20737  aspval2  21941  fvmptnn04if  22876  ntreq0  23106  cmpcov2  23419  llyi  23503  nllyi  23504  ptpjpre1  23600  tx1cn  23638  tx2cn  23639  txtube  23669  txkgen  23681  trfil2  23916  elflim2  23993  cnpflfi  24028  isfcls  24038  cnextcn  24096  istlm  24214  blres  24462  metrest  24558  isnlm  24717  elpi1  25097  isclmp  25149  iscvsp  25180  isncvsngp  25202  iscph  25223  cfilucfil3  25373  itg1climres  25769  itgsubst  26110  ulmdvlem3  26463  cubic  26910  vmasum  27278  lgsquadlem1  27442  lgsquadlem2  27443  sltval2  27719  madeval2  27910  legov  28611  perpln1  28736  axcontlem5  29001  nbgrel  29375  nbusgredgeu0  29403  nb3grpr2  29418  finsumvtxdg2ssteplem3  29583  usgr2pth0  29801  isclwlke  29813  wwlksnfi  29939  elwwlks2ons3  29988  wpthswwlks2on  29994  usgr2wspthon  29998  rusgrnumwwlkl1  30001  isclwwlk  30016  isclwwlknx  30068  clwlknf1oclwwlkn  30116  clwwlknonel  30127  clwwlknon2x  30135  clwwlkvbij  30145  iseupthf1o  30234  fusgr2wsp2nb  30366  grpoidinvlem3  30538  h2hlm  31012  issh  31240  issh3  31251  ocsh  31315  cvbr2  32315  cvnbtwn2  32319  mdsl2i  32354  cvmdi  32356  mdsymlem2  32436  sumdmdii  32447  dmrab  32525  difrab2  32526  disjunsn  32616  mpomptxf  32695  ressupprn  32702  1stpreima  32718  2ndpreima  32719  f1od2  32735  nndiffz1  32791  omndmul2  33062  1arithufdlem4  33540  r1plmhm  33595  r1pquslmic  33596  smatrcl  33742  crefdf  33794  1stmbfm  34225  2ndmbfm  34226  dya2iocnei  34247  eulerpartlemgvv  34341  eulerpartlemn  34346  bnj250  34677  bnj251  34678  bnj256  34682  bnj168  34706  cusgr3cyclex  35104  iscvm  35227  axacprim  35669  dfdm5  35736  dfrn5  35737  elima4  35739  dfon3  35856  brimg  35901  dfrecs2  35914  dfrdg4  35915  ifscgr  36008  cgrxfr  36019  segcon2  36069  seglecgr12im  36074  segletr  36078  ellines  36116  neifg  36337  bj-dfmpoa  37084  bj-imdiridlem  37151  bj-imdirco  37156  topdifinffinlem  37313  icorempo  37317  difunieq  37340  finxpreclem6  37362  wl-df4-3mintru2  37453  wl-cases2-dnf  37466  curf  37558  uncf  37559  matunitlindflem2  37577  matunitlindf  37578  poimirlem26  37606  poimirlem28  37608  poimirlem30  37610  poimirlem32  37612  poimir  37613  itg2addnc  37634  ftc1anclem5  37657  ftc1anc  37661  areacirclem5  37672  isbnd2  37743  heibor1  37770  anan  38183  br1cnvres  38225  inxpxrn  38351  prtlem70  38813  prtlem100  38815  lsateln0  38951  islshpat  38973  lcvbr2  38978  lcvnbtwn2  38983  isopos  39136  cvrval2  39230  cvrnbtwn2  39231  ishlat2  39309  3dim0  39414  islvol5  39536  pmapjat1  39810  pclcmpatN  39858  pclfinclN  39907  cdlemefrs29pre00  40352  cdlemefrs29bpre0  40353  cdlemefrs29cpre1  40355  cdleme32a  40398  cdlemftr3  40522  dvhopellsm  41074  dibelval3  41104  diblsmopel  41128  mapdvalc  41586  mapdval4N  41589  mapdordlem1a  41591  3factsumint2  41979  3factsumint3  41980  3factsumint4  41981  3factsumint  41982  aks4d1p8  42044  fimgmcyc  42489  fsuppind  42545  diophrex  42731  rmxdioph  42973  dford4  42986  islmodfg  43026  islssfg2  43028  fgraphopab  43164  cantnftermord  43282  tfsconcatlem  43298  k0004lem1  44109  ismnuprim  44263  2sbc5g  44385  limcrecl  45550  dvnmul  45864  dvnprodlem2  45868  fourierdlem83  46110  iundjiun  46381  fcoresf1ob  46988  f1ocof1ob  46996  4an21  47185  sprvalpwn0  47357  pairreueq  47384  prprsprreu  47393  prprreueq  47394  clnbgrel  47701  dfvopnbgr2  47725  rngcinvALTV  47999  ringcinvALTV  48033  mpomptx2  48059  opnneir  48586  opnneilv  48588  i0oii  48599  io1ii  48600  iscnrm3lem3  48615