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  1095  3an4anass  1105  4anpull2  1362  an33rean  1485  2sb5  2278  r19.41v  3189  r3ex  3198  r19.41  3263  rabrabi  3456  rabrab  3461  ceqsex3v  3537  spc2ed  3601  ceqsrex2v  3658  rexrab  3702  rexrab2  3706  reurab  3707  2reu5  3764  rexssOLD  4061  inass  4228  rexin  4250  difin2  4301  difrab  4318  reupick3  4330  inssdif0  4374  rabsneq  4644  rexdifpr  4659  rexdifsn  4794  reusv2lem4  5401  reusv2  5403  eqvinop  5492  copsexgw  5495  copsexg  5496  rabxp  5733  elvvv  5761  resopab2  6054  difxp  6184  mptpreima  6258  resco  6270  coass  6285  dfpo2  6316  frpoind  6363  wfiOLD  6372  imadif  6650  dff1o2  6853  eqfnfv3  7053  f1ossf1o  7148  isoini  7358  f1oiso  7371  riotarab  7430  oprabidw  7462  oprabid  7463  dfoprab2  7491  mpoeq123  7505  mpomptx  7546  resoprab2  7552  ov3  7596  uniuni  7782  elxp4  7944  elxp5  7945  oprabex3  8002  frxp  8151  rexsupp  8207  brtpos2  8257  oeeui  8640  oeeu  8641  omabs  8689  eldifsucnn  8702  naddsuc2  8739  mapsnend  9076  xpsnen  9095  xpcomco  9102  xpassen  9106  wemapsolem  9590  epfrs  9771  frind  9790  aceq1  10157  dfac5lem1  10163  dfac5lem2  10164  dfac5lem5  10167  kmlem3  10193  kmlem14  10204  pwfseqlem1  10698  ltexpi  10942  ltexprlem4  11079  axaddf  11185  axmulf  11186  rexuz  12940  rexuz2  12941  nnwos  12957  zmin  12986  rexrp  13056  elixx3g  13400  elfz2  13554  preduz  13690  fzind2  13824  hashbclem  14491  resqrex  15289  rlim  15531  divalglem10  16439  divalgb  16441  gcdass  16584  lcmass  16651  isprm2  16719  infpn2  16951  ispos2  18361  issubmndb  18818  issubg3  19162  resscntz  19351  subgdmdprd  20054  dprd2d2  20064  isrnghm  20441  isrnghmmul  20442  dfrhm2  20474  rngcinv  20637  ringcinv  20671  isdomn3  20715  aspval2  21918  fvmptnn04if  22855  ntreq0  23085  cmpcov2  23398  llyi  23482  nllyi  23483  ptpjpre1  23579  tx1cn  23617  tx2cn  23618  txtube  23648  txkgen  23660  trfil2  23895  elflim2  23972  cnpflfi  24007  isfcls  24017  cnextcn  24075  istlm  24193  blres  24441  metrest  24537  isnlm  24696  elpi1  25078  isclmp  25130  iscvsp  25161  isncvsngp  25183  iscph  25204  cfilucfil3  25354  itg1climres  25749  itgsubst  26090  ulmdvlem3  26445  cubic  26892  vmasum  27260  lgsquadlem1  27424  lgsquadlem2  27425  sltval2  27701  madeval2  27892  legov  28593  perpln1  28718  axcontlem5  28983  nbgrel  29357  nbusgredgeu0  29385  nb3grpr2  29400  finsumvtxdg2ssteplem3  29565  usgr2pth0  29785  isclwlke  29797  wwlksnfi  29926  elwwlks2ons3  29975  wpthswwlks2on  29981  usgr2wspthon  29985  rusgrnumwwlkl1  29988  isclwwlk  30003  isclwwlknx  30055  clwlknf1oclwwlkn  30103  clwwlknonel  30114  clwwlknon2x  30122  clwwlkvbij  30132  iseupthf1o  30221  fusgr2wsp2nb  30353  grpoidinvlem3  30525  h2hlm  30999  issh  31227  issh3  31238  ocsh  31302  cvbr2  32302  cvnbtwn2  32306  mdsl2i  32341  cvmdi  32343  mdsymlem2  32423  sumdmdii  32434  dmrab  32516  difrab2  32517  disjunsn  32607  mpomptxf  32687  ressupprn  32699  1stpreima  32716  2ndpreima  32717  f1od2  32732  nndiffz1  32788  omndmul2  33089  1arithufdlem4  33575  r1plmhm  33630  r1pquslmic  33631  smatrcl  33795  crefdf  33847  1stmbfm  34262  2ndmbfm  34263  dya2iocnei  34284  eulerpartlemgvv  34378  eulerpartlemn  34383  bnj250  34715  bnj251  34716  bnj256  34720  bnj168  34744  cusgr3cyclex  35141  iscvm  35264  axacprim  35707  dfdm5  35773  dfrn5  35774  elima4  35776  dfon3  35893  brimg  35938  dfrecs2  35951  dfrdg4  35952  ifscgr  36045  cgrxfr  36056  segcon2  36106  seglecgr12im  36111  segletr  36115  ellines  36153  neifg  36372  bj-dfmpoa  37119  bj-imdiridlem  37186  bj-imdirco  37191  topdifinffinlem  37348  icorempo  37352  difunieq  37375  finxpreclem6  37397  wl-df4-3mintru2  37488  wl-cases2-dnf  37513  curf  37605  uncf  37606  matunitlindflem2  37624  matunitlindf  37625  poimirlem26  37653  poimirlem28  37655  poimirlem30  37657  poimirlem32  37659  poimir  37660  itg2addnc  37681  ftc1anclem5  37704  ftc1anc  37708  areacirclem5  37719  isbnd2  37790  heibor1  37817  anan  38230  br1cnvres  38270  inxpxrn  38396  prtlem70  38858  prtlem100  38860  lsateln0  38996  islshpat  39018  lcvbr2  39023  lcvnbtwn2  39028  isopos  39181  cvrval2  39275  cvrnbtwn2  39276  ishlat2  39354  3dim0  39459  islvol5  39581  pmapjat1  39855  pclcmpatN  39903  pclfinclN  39952  cdlemefrs29pre00  40397  cdlemefrs29bpre0  40398  cdlemefrs29cpre1  40400  cdleme32a  40443  cdlemftr3  40567  dvhopellsm  41119  dibelval3  41149  diblsmopel  41173  mapdvalc  41631  mapdval4N  41634  mapdordlem1a  41636  3factsumint2  42023  3factsumint3  42024  3factsumint4  42025  3factsumint  42026  aks4d1p8  42088  redvmptabs  42390  fimgmcyc  42544  fsuppind  42600  diophrex  42786  rmxdioph  43028  dford4  43041  islmodfg  43081  islssfg2  43083  fgraphopab  43215  cantnftermord  43333  tfsconcatlem  43349  k0004lem1  44160  ismnuprim  44313  2sbc5g  44435  modelaxreplem3  44997  limcrecl  45644  dvnmul  45958  dvnprodlem2  45962  fourierdlem83  46204  iundjiun  46475  fcoresf1ob  47085  f1ocof1ob  47093  4an21  47282  sprvalpwn0  47470  pairreueq  47497  prprsprreu  47506  prprreueq  47507  clnbgrel  47815  dfvopnbgr2  47839  rngcinvALTV  48192  ringcinvALTV  48226  mpomptx2  48251  reuxfr1dd  48726  coxp  48744  opnneir  48804  opnneilv  48806  i0oii  48817  io1ii  48818  upfval2  48934