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 208	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  bianass  641  an31  647  an4  655  3anass  1093  3an4anass  1103  an33rean  1480  2sb5  2267  r19.41v  3184  r19.41  3256  rabrabi  3446  rabrab  3451  ceqsex3v  3528  spc2ed  3587  ceqsrex2v  3643  rexrab  3690  rexrab2  3694  reurab  3695  2reu5  3752  rexss  4051  inass  4215  rexin  4235  indifdirOLD  4281  difin2  4287  difrab  4304  reupick3  4315  inssdif0  4365  rexdifpr  4657  rexdifsn  4793  reusv2lem4  5395  reusv2  5397  eqvinop  5483  copsexgw  5486  copsexg  5487  rabxp  5720  elvvv  5747  resopab2  6034  difxp  6162  mptpreima  6236  resco  6248  coass  6263  dfpo2  6294  frpoind  6342  wfiOLD  6351  imadif  6631  dff1o2  6838  eqfnfv3  7036  f1ossf1o  7131  isoini  7340  f1oiso  7353  riotarab  7413  oprabidw  7445  oprabid  7446  dfoprab2  7472  mpoeq123  7486  mpomptx  7527  resoprab2  7533  ov3  7578  uniuni  7758  elxp4  7924  elxp5  7925  oprabex3  7975  frxp  8125  rexsupp  8180  brtpos2  8231  oeeui  8616  oeeu  8617  omabs  8665  eldifsucnn  8678  mapsnend  9054  xpsnen  9073  xpcomco  9080  xpassen  9084  wemapsolem  9567  epfrs  9748  frind  9767  aceq1  10134  dfac5lem1  10140  dfac5lem2  10141  dfac5lem5  10144  kmlem3  10169  kmlem14  10180  pwfseqlem1  10675  ltexpi  10919  ltexprlem4  11056  axaddf  11162  axmulf  11163  rexuz  12906  rexuz2  12907  nnwos  12923  zmin  12952  rexrp  13021  elixx3g  13363  elfz2  13517  preduz  13649  fzind2  13776  hashbclem  14437  resqrex  15223  rlim  15465  divalglem10  16372  divalgb  16374  gcdass  16516  lcmass  16578  isprm2  16646  infpn2  16875  ispos2  18300  issubmndb  18750  issubg3  19092  resscntz  19277  subgdmdprd  19984  dprd2d2  19994  isrnghm  20373  isrnghmmul  20374  dfrhm2  20406  rngcinv  20563  ringcinv  20597  isdomn3  21241  aspval2  21824  fvmptnn04if  22744  ntreq0  22974  cmpcov2  23287  llyi  23371  nllyi  23372  ptpjpre1  23468  tx1cn  23506  tx2cn  23507  txtube  23537  txkgen  23549  trfil2  23784  elflim2  23861  cnpflfi  23896  isfcls  23906  cnextcn  23964  istlm  24082  blres  24330  metrest  24426  isnlm  24585  elpi1  24965  isclmp  25017  iscvsp  25048  isncvsngp  25070  iscph  25091  cfilucfil3  25241  itg1climres  25637  itgsubst  25977  ulmdvlem3  26331  cubic  26774  vmasum  27142  lgsquadlem1  27306  lgsquadlem2  27307  sltval2  27582  madeval2  27773  legov  28382  perpln1  28507  axcontlem5  28772  nbgrel  29146  nbusgredgeu0  29174  nb3grpr2  29189  finsumvtxdg2ssteplem3  29354  usgr2pth0  29572  isclwlke  29584  wwlksnfi  29710  elwwlks2ons3  29759  wpthswwlks2on  29765  usgr2wspthon  29769  rusgrnumwwlkl1  29772  isclwwlk  29787  isclwwlknx  29839  clwlknf1oclwwlkn  29887  clwwlknonel  29898  clwwlknon2x  29906  clwwlkvbij  29916  iseupthf1o  30005  fusgr2wsp2nb  30137  grpoidinvlem3  30309  h2hlm  30783  issh  31011  issh3  31022  ocsh  31086  cvbr2  32086  cvnbtwn2  32090  mdsl2i  32125  cvmdi  32127  mdsymlem2  32207  sumdmdii  32218  dmrab  32288  difrab2  32289  disjunsn  32377  mpomptxf  32457  ressupprn  32464  1stpreima  32480  2ndpreima  32481  f1od2  32497  nndiffz1  32548  omndmul2  32786  r1plmhm  33270  r1pquslmic  33271  smatrcl  33391  crefdf  33443  1stmbfm  33874  2ndmbfm  33875  dya2iocnei  33896  eulerpartlemgvv  33990  eulerpartlemn  33995  bnj250  34326  bnj251  34327  bnj256  34331  bnj168  34355  cusgr3cyclex  34740  iscvm  34863  axacprim  35295  dfdm5  35362  dfrn5  35363  elima4  35365  dfon3  35482  brimg  35527  dfrecs2  35540  dfrdg4  35541  ifscgr  35634  cgrxfr  35645  segcon2  35695  seglecgr12im  35700  segletr  35704  ellines  35742  neifg  35849  bj-dfmpoa  36591  bj-imdiridlem  36658  bj-imdirco  36663  topdifinffinlem  36820  icorempo  36824  difunieq  36847  finxpreclem6  36869  wl-df4-3mintru2  36960  wl-cases2-dnf  36973  curf  37065  uncf  37066  matunitlindflem2  37084  matunitlindf  37085  poimirlem26  37113  poimirlem28  37115  poimirlem30  37117  poimirlem32  37119  poimir  37120  itg2addnc  37141  ftc1anclem5  37164  ftc1anc  37168  areacirclem5  37179  isbnd2  37250  heibor1  37277  anan  37692  br1cnvres  37735  inxpxrn  37861  prtlem70  38323  prtlem100  38325  lsateln0  38461  islshpat  38483  lcvbr2  38488  lcvnbtwn2  38493  isopos  38646  cvrval2  38740  cvrnbtwn2  38741  ishlat2  38819  3dim0  38924  islvol5  39046  pmapjat1  39320  pclcmpatN  39368  pclfinclN  39417  cdlemefrs29pre00  39862  cdlemefrs29bpre0  39863  cdlemefrs29cpre1  39865  cdleme32a  39908  cdlemftr3  40032  dvhopellsm  40584  dibelval3  40614  diblsmopel  40638  mapdvalc  41096  mapdval4N  41099  mapdordlem1a  41101  3factsumint2  41487  3factsumint3  41488  3factsumint4  41489  3factsumint  41490  aks4d1p8  41552  fsuppind  41817  diophrex  42189  rmxdioph  42431  dford4  42444  islmodfg  42487  islssfg2  42489  fgraphopab  42625  cantnftermord  42743  tfsconcatlem  42759  naddsuc2  42816  k0004lem1  43571  ismnuprim  43725  2sbc5g  43847  limcrecl  45011  dvnmul  45325  dvnprodlem2  45329  fourierdlem83  45571  iundjiun  45842  fcoresf1ob  46449  f1ocof1ob  46455  4an21  46644  sprvalpwn0  46817  pairreueq  46844  prprsprreu  46853  prprreueq  46854  rngcinvALTV  47332  ringcinvALTV  47366  mpomptx2  47392  opnneir  47919  opnneilv  47921  i0oii  47932  io1ii  47933  iscnrm3lem3  47948