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  4anpull2  1362  an33rean  1485  2sb5  2280  r19.41v  3162  r3ex  3171  r19.41  3236  rabrabi  3414  rabrab  3419  ceqsex3v  3491  spc2ed  3551  ceqsrex2v  3608  rexrab  3650  rexrab2  3654  reurab  3655  2reu5  3712  rexssOLD  4007  inass  4175  rexin  4197  difin2  4248  difrab  4265  reupick3  4277  inssdif0  4321  rabsneq  4592  rexdifpr  4609  rexdifsn  4743  reusv2lem4  5337  reusv2  5339  eqvinop  5425  copsexgw  5428  copsexg  5429  rabxp  5662  elvvv  5690  resopab2  5984  difxp  6111  mptpreima  6185  resco  6197  coass  6213  dfpo2  6243  frpoind  6289  imadif  6565  dff1o2  6768  eqfnfv3  6966  f1ossf1o  7061  isoini  7272  f1oiso  7285  riotarab  7345  oprabidw  7377  oprabid  7378  dfoprab2  7404  mpoeq123  7418  mpomptx  7459  resoprab2  7465  ov3  7509  uniuni  7695  elxp4  7852  elxp5  7853  oprabex3  7909  frxp  8056  rexsupp  8112  brtpos2  8162  oeeui  8517  oeeu  8518  omabs  8566  eldifsucnn  8579  naddsuc2  8616  mapsnend  8958  xpsnen  8974  xpcomco  8980  xpassen  8984  wemapsolem  9436  epfrs  9621  frind  9643  aceq1  10008  dfac5lem1  10014  dfac5lem2  10015  dfac5lem5  10018  kmlem3  10044  kmlem14  10055  pwfseqlem1  10549  ltexpi  10793  ltexprlem4  10930  axaddf  11036  axmulf  11037  rexuz  12796  rexuz2  12797  nnwos  12813  zmin  12842  rexrp  12913  elixx3g  13258  elfz2  13414  preduz  13550  fzind2  13688  hashbclem  14359  resqrex  15157  rlim  15402  divalglem10  16313  divalgb  16315  gcdass  16458  lcmass  16525  isprm2  16593  infpn2  16825  ispos2  18221  issubmndb  18713  issubg3  19057  resscntz  19245  subgdmdprd  19948  dprd2d2  19958  omndmul2  20045  isrnghm  20359  isrnghmmul  20360  dfrhm2  20392  rngcinv  20552  ringcinv  20586  isdomn3  20630  aspval2  21835  fvmptnn04if  22764  ntreq0  22992  cmpcov2  23305  llyi  23389  nllyi  23390  ptpjpre1  23486  tx1cn  23524  tx2cn  23525  txtube  23555  txkgen  23567  trfil2  23802  elflim2  23879  cnpflfi  23914  isfcls  23924  cnextcn  23982  istlm  24100  blres  24346  metrest  24439  isnlm  24590  elpi1  24972  isclmp  25024  iscvsp  25055  isncvsngp  25076  iscph  25097  cfilucfil3  25247  itg1climres  25642  itgsubst  25983  ulmdvlem3  26338  cubic  26786  vmasum  27154  lgsquadlem1  27318  lgsquadlem2  27319  sltval2  27595  madeval2  27794  legov  28563  perpln1  28688  axcontlem5  28946  nbgrel  29318  nbusgredgeu0  29346  nb3grpr2  29361  finsumvtxdg2ssteplem3  29526  usgr2pth0  29743  isclwlke  29755  wwlksnfi  29884  elwwlks2ons3  29933  wpthswwlks2on  29942  usgr2wspthon  29946  rusgrnumwwlkl1  29949  isclwwlk  29964  isclwwlknx  30016  clwlknf1oclwwlkn  30064  clwwlknonel  30075  clwwlknon2x  30083  clwwlkvbij  30093  iseupthf1o  30182  fusgr2wsp2nb  30314  grpoidinvlem3  30486  h2hlm  30960  issh  31188  issh3  31199  ocsh  31263  cvbr2  32263  cvnbtwn2  32267  mdsl2i  32302  cvmdi  32304  mdsymlem2  32384  sumdmdii  32395  dmrab  32476  difrab2  32477  disjunsn  32574  mpomptxf  32659  ressupprn  32671  1stpreima  32688  2ndpreima  32689  f1od2  32702  nndiffz1  32769  1arithufdlem4  33512  r1plmhm  33570  r1pquslmic  33571  extdgfialglem1  33705  smatrcl  33809  crefdf  33861  1stmbfm  34273  2ndmbfm  34274  dya2iocnei  34295  eulerpartlemgvv  34389  eulerpartlemn  34394  bnj250  34713  bnj251  34714  bnj256  34718  bnj168  34742  cusgr3cyclex  35180  iscvm  35303  axacprim  35751  dfdm5  35817  dfrn5  35818  elima4  35820  dfon3  35934  brimg  35979  dfrecs2  35994  dfrdg4  35995  ifscgr  36088  cgrxfr  36099  segcon2  36149  seglecgr12im  36154  segletr  36158  ellines  36196  neifg  36415  bj-dfmpoa  37162  bj-imdiridlem  37229  bj-imdirco  37234  topdifinffinlem  37391  icorempo  37395  difunieq  37418  finxpreclem6  37440  wl-df4-3mintru2  37531  wl-cases2-dnf  37556  curf  37637  uncf  37638  matunitlindflem2  37656  matunitlindf  37657  poimirlem26  37685  poimirlem28  37687  poimirlem30  37689  poimirlem32  37691  poimir  37692  itg2addnc  37713  ftc1anclem5  37736  ftc1anc  37740  areacirclem5  37751  isbnd2  37822  heibor1  37849  anan  38269  br1cnvres  38305  inxpxrn  38441  prtlem70  38955  prtlem100  38957  lsateln0  39093  islshpat  39115  lcvbr2  39120  lcvnbtwn2  39125  isopos  39278  cvrval2  39372  cvrnbtwn2  39373  ishlat2  39451  3dim0  39555  islvol5  39677  pmapjat1  39951  pclcmpatN  39999  pclfinclN  40048  cdlemefrs29pre00  40493  cdlemefrs29bpre0  40494  cdlemefrs29cpre1  40496  cdleme32a  40539  cdlemftr3  40663  dvhopellsm  41215  dibelval3  41245  diblsmopel  41269  mapdvalc  41727  mapdval4N  41730  mapdordlem1a  41732  3factsumint2  42114  3factsumint3  42115  3factsumint4  42116  3factsumint  42117  aks4d1p8  42179  redvmptabs  42452  fimgmcyc  42626  fsuppind  42682  diophrex  42867  rmxdioph  43108  dford4  43121  islmodfg  43161  islssfg2  43163  fgraphopab  43295  cantnftermord  43412  tfsconcatlem  43428  k0004lem1  44239  ismnuprim  44386  2sbc5g  44508  modelaxreplem3  45072  limcrecl  45728  dvnmul  46040  dvnprodlem2  46044  fourierdlem83  46286  iundjiun  46557  fcoresf1ob  47172  f1ocof1ob  47180  4an21  47369  sprvalpwn0  47582  pairreueq  47609  prprsprreu  47618  prprreueq  47619  clnbgrel  47927  dfvopnbgr2  47952  rngcinvALTV  48375  ringcinvALTV  48409  mpomptx2  48434  reuxfr1dd  48906  coxp  48932  opnneir  49006  opnneilv  49008  i0oii  49019  io1ii  49020  upfval2  49277