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  642  an31  648  an4  656  3anass  1094  3an4anass  1104  an33rean  1482  2sb5  2275  r19.41v  3186  r3ex  3195  r19.41  3260  rabrabi  3452  rabrab  3457  ceqsex3v  3536  spc2ed  3600  ceqsrex2v  3657  rexrab  3704  rexrab2  3708  reurab  3709  2reu5  3766  rexss  4070  inass  4235  rexin  4255  difin2  4306  difrab  4323  reupick3  4335  inssdif0  4379  rabsneq  4648  rexdifpr  4663  rexdifsn  4798  reusv2lem4  5406  reusv2  5408  eqvinop  5497  copsexgw  5500  copsexg  5501  rabxp  5736  elvvv  5763  resopab2  6055  difxp  6185  mptpreima  6259  resco  6271  coass  6286  dfpo2  6317  frpoind  6364  wfiOLD  6373  imadif  6651  dff1o2  6853  eqfnfv3  7052  f1ossf1o  7147  isoini  7357  f1oiso  7370  riotarab  7429  oprabidw  7461  oprabid  7462  dfoprab2  7490  mpoeq123  7504  mpomptx  7545  resoprab2  7551  ov3  7595  uniuni  7780  elxp4  7944  elxp5  7945  oprabex3  8000  frxp  8149  rexsupp  8205  brtpos2  8255  oeeui  8638  oeeu  8639  omabs  8687  eldifsucnn  8700  naddsuc2  8737  mapsnend  9074  xpsnen  9093  xpcomco  9100  xpassen  9104  wemapsolem  9587  epfrs  9768  frind  9787  aceq1  10154  dfac5lem1  10160  dfac5lem2  10161  dfac5lem5  10164  kmlem3  10190  kmlem14  10201  pwfseqlem1  10695  ltexpi  10939  ltexprlem4  11076  axaddf  11182  axmulf  11183  rexuz  12937  rexuz2  12938  nnwos  12954  zmin  12983  rexrp  13053  elixx3g  13396  elfz2  13550  preduz  13686  fzind2  13820  hashbclem  14487  resqrex  15285  rlim  15527  divalglem10  16435  divalgb  16437  gcdass  16580  lcmass  16647  isprm2  16715  infpn2  16946  ispos2  18372  issubmndb  18830  issubg3  19174  resscntz  19363  subgdmdprd  20068  dprd2d2  20078  isrnghm  20457  isrnghmmul  20458  dfrhm2  20490  rngcinv  20653  ringcinv  20687  isdomn3  20731  aspval2  21935  fvmptnn04if  22870  ntreq0  23100  cmpcov2  23413  llyi  23497  nllyi  23498  ptpjpre1  23594  tx1cn  23632  tx2cn  23633  txtube  23663  txkgen  23675  trfil2  23910  elflim2  23987  cnpflfi  24022  isfcls  24032  cnextcn  24090  istlm  24208  blres  24456  metrest  24552  isnlm  24711  elpi1  25091  isclmp  25143  iscvsp  25174  isncvsngp  25196  iscph  25217  cfilucfil3  25367  itg1climres  25763  itgsubst  26104  ulmdvlem3  26459  cubic  26906  vmasum  27274  lgsquadlem1  27438  lgsquadlem2  27439  sltval2  27715  madeval2  27906  legov  28607  perpln1  28732  axcontlem5  28997  nbgrel  29371  nbusgredgeu0  29399  nb3grpr2  29414  finsumvtxdg2ssteplem3  29579  usgr2pth0  29797  isclwlke  29809  wwlksnfi  29935  elwwlks2ons3  29984  wpthswwlks2on  29990  usgr2wspthon  29994  rusgrnumwwlkl1  29997  isclwwlk  30012  isclwwlknx  30064  clwlknf1oclwwlkn  30112  clwwlknonel  30123  clwwlknon2x  30131  clwwlkvbij  30141  iseupthf1o  30230  fusgr2wsp2nb  30362  grpoidinvlem3  30534  h2hlm  31008  issh  31236  issh3  31247  ocsh  31311  cvbr2  32311  cvnbtwn2  32315  mdsl2i  32350  cvmdi  32352  mdsymlem2  32432  sumdmdii  32443  dmrab  32524  difrab2  32525  disjunsn  32613  mpomptxf  32693  ressupprn  32704  1stpreima  32721  2ndpreima  32722  f1od2  32738  nndiffz1  32794  omndmul2  33071  1arithufdlem4  33554  r1plmhm  33609  r1pquslmic  33610  smatrcl  33756  crefdf  33808  1stmbfm  34241  2ndmbfm  34242  dya2iocnei  34263  eulerpartlemgvv  34357  eulerpartlemn  34362  bnj250  34693  bnj251  34694  bnj256  34698  bnj168  34722  cusgr3cyclex  35120  iscvm  35243  axacprim  35686  dfdm5  35753  dfrn5  35754  elima4  35756  dfon3  35873  brimg  35918  dfrecs2  35931  dfrdg4  35932  ifscgr  36025  cgrxfr  36036  segcon2  36086  seglecgr12im  36091  segletr  36095  ellines  36133  neifg  36353  bj-dfmpoa  37100  bj-imdiridlem  37167  bj-imdirco  37172  topdifinffinlem  37329  icorempo  37333  difunieq  37356  finxpreclem6  37378  wl-df4-3mintru2  37469  wl-cases2-dnf  37492  curf  37584  uncf  37585  matunitlindflem2  37603  matunitlindf  37604  poimirlem26  37632  poimirlem28  37634  poimirlem30  37636  poimirlem32  37638  poimir  37639  itg2addnc  37660  ftc1anclem5  37683  ftc1anc  37687  areacirclem5  37698  isbnd2  37769  heibor1  37796  anan  38209  br1cnvres  38250  inxpxrn  38376  prtlem70  38838  prtlem100  38840  lsateln0  38976  islshpat  38998  lcvbr2  39003  lcvnbtwn2  39008  isopos  39161  cvrval2  39255  cvrnbtwn2  39256  ishlat2  39334  3dim0  39439  islvol5  39561  pmapjat1  39835  pclcmpatN  39883  pclfinclN  39932  cdlemefrs29pre00  40377  cdlemefrs29bpre0  40378  cdlemefrs29cpre1  40380  cdleme32a  40423  cdlemftr3  40547  dvhopellsm  41099  dibelval3  41129  diblsmopel  41153  mapdvalc  41611  mapdval4N  41614  mapdordlem1a  41616  3factsumint2  42003  3factsumint3  42004  3factsumint4  42005  3factsumint  42006  aks4d1p8  42068  redvmptabs  42368  fimgmcyc  42520  fsuppind  42576  diophrex  42762  rmxdioph  43004  dford4  43017  islmodfg  43057  islssfg2  43059  fgraphopab  43191  cantnftermord  43309  tfsconcatlem  43325  k0004lem1  44136  ismnuprim  44289  2sbc5g  44411  modelaxreplem3  44944  limcrecl  45584  dvnmul  45898  dvnprodlem2  45902  fourierdlem83  46144  iundjiun  46415  fcoresf1ob  47022  f1ocof1ob  47030  4an21  47219  sprvalpwn0  47407  pairreueq  47434  prprsprreu  47443  prprreueq  47444  clnbgrel  47752  dfvopnbgr2  47776  rngcinvALTV  48119  ringcinvALTV  48153  mpomptx2  48179  reuxfr1dd  48654  opnneir  48702  opnneilv  48704  i0oii  48715  io1ii  48716  iscnrm3lem3  48731