Theorem anass 470

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 469	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		id 22	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	anasss 468	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	2, 4	impbii 208	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ wa 397

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 398

This theorem is referenced by:  bianass  641  an31  647  an4  655  3anass  1096  3an4anass  1106  an33rean  1484  2sb5  2272  r19.41v  3189  r19.41  3261  rabrabi  3451  rabrab  3456  ceqsex3v  3531  spc2ed  3591  ceqsrex2v  3645  rexrab  3691  rexrab2  3695  reurab  3696  2reu5  3753  rexss  4054  inass  4218  rexin  4238  indifdirOLD  4284  difin2  4290  difrab  4307  reupick3  4318  inssdif0  4368  rexdifpr  4660  rexdifsn  4796  reusv2lem4  5398  reusv2  5400  eqvinop  5486  copsexgw  5489  copsexg  5490  rabxp  5722  elvvv  5749  resopab2  6034  difxp  6160  mptpreima  6234  resco  6246  coass  6261  dfpo2  6292  frpoind  6340  wfiOLD  6349  imadif  6629  dff1o2  6835  eqfnfv3  7030  f1ossf1o  7121  isoini  7330  f1oiso  7343  riotarab  7403  oprabidw  7435  oprabid  7436  dfoprab2  7462  mpoeq123  7476  mpomptx  7516  resoprab2  7522  ov3  7565  uniuni  7744  elxp4  7908  elxp5  7909  oprabex3  7959  frxp  8107  rexsupp  8162  brtpos2  8212  oeeui  8598  oeeu  8599  omabs  8646  eldifsucnn  8659  mapsnend  9032  xpsnen  9051  xpcomco  9058  xpassen  9062  wemapsolem  9541  epfrs  9722  frind  9741  aceq1  10108  dfac5lem1  10114  dfac5lem2  10115  dfac5lem5  10118  kmlem3  10143  kmlem14  10154  pwfseqlem1  10649  ltexpi  10893  ltexprlem4  11030  axaddf  11136  axmulf  11137  rexuz  12878  rexuz2  12879  nnwos  12895  zmin  12924  rexrp  12991  elixx3g  13333  elfz2  13487  preduz  13619  fzind2  13746  hashbclem  14407  resqrex  15193  rlim  15435  divalglem10  16341  divalgb  16343  gcdass  16485  lcmass  16547  isprm2  16615  infpn2  16842  ispos2  18264  issubmndb  18682  issubg3  19018  resscntz  19190  subgdmdprd  19896  dprd2d2  19906  dfrhm2  20242  aspval2  21434  fvmptnn04if  22333  ntreq0  22563  cmpcov2  22876  llyi  22960  nllyi  22961  ptpjpre1  23057  tx1cn  23095  tx2cn  23096  txtube  23126  txkgen  23138  trfil2  23373  elflim2  23450  cnpflfi  23485  isfcls  23495  cnextcn  23553  istlm  23671  blres  23919  metrest  24015  isnlm  24174  elpi1  24543  isclmp  24595  iscvsp  24626  isncvsngp  24648  iscph  24669  cfilucfil3  24819  itg1climres  25214  itgsubst  25548  ulmdvlem3  25896  cubic  26334  vmasum  26699  lgsquadlem1  26863  lgsquadlem2  26864  sltval2  27139  madeval2  27328  legov  27816  perpln1  27941  axcontlem5  28206  nbgrel  28577  nbusgredgeu0  28605  nb3grpr2  28620  finsumvtxdg2ssteplem3  28784  usgr2pth0  29002  isclwlke  29014  wwlksnfi  29140  elwwlks2ons3  29189  wpthswwlks2on  29195  usgr2wspthon  29199  rusgrnumwwlkl1  29202  isclwwlk  29217  isclwwlknx  29269  clwlknf1oclwwlkn  29317  clwwlknonel  29328  clwwlknon2x  29336  clwwlkvbij  29346  iseupthf1o  29435  fusgr2wsp2nb  29567  grpoidinvlem3  29737  h2hlm  30211  issh  30439  issh3  30450  ocsh  30514  cvbr2  31514  cvnbtwn2  31518  mdsl2i  31553  cvmdi  31555  mdsymlem2  31635  sumdmdii  31646  dmrab  31715  difrab2  31716  disjunsn  31803  mpomptxf  31883  ressupprn  31890  1stpreima  31906  2ndpreima  31907  f1od2  31924  nndiffz1  31975  omndmul2  32208  smatrcl  32714  crefdf  32766  1stmbfm  33197  2ndmbfm  33198  dya2iocnei  33219  eulerpartlemgvv  33313  eulerpartlemn  33318  bnj250  33650  bnj251  33651  bnj256  33655  bnj168  33679  cusgr3cyclex  34065  iscvm  34188  axacprim  34614  dfdm5  34682  dfrn5  34683  elima4  34685  dfon3  34802  brimg  34847  dfrecs2  34860  dfrdg4  34861  ifscgr  34954  cgrxfr  34965  segcon2  35015  seglecgr12im  35020  segletr  35024  ellines  35062  neifg  35194  bj-dfmpoa  35937  bj-imdiridlem  36004  bj-imdirco  36009  topdifinffinlem  36166  icorempo  36170  difunieq  36193  finxpreclem6  36215  wl-df4-3mintru2  36306  wl-cases2-dnf  36319  curf  36404  uncf  36405  matunitlindflem2  36423  matunitlindf  36424  poimirlem26  36452  poimirlem28  36454  poimirlem30  36456  poimirlem32  36458  poimir  36459  itg2addnc  36480  ftc1anclem5  36503  ftc1anc  36507  areacirclem5  36518  isbnd2  36589  heibor1  36616  anan  37031  br1cnvres  37075  inxpxrn  37203  prtlem70  37665  prtlem100  37667  lsateln0  37803  islshpat  37825  lcvbr2  37830  lcvnbtwn2  37835  isopos  37988  cvrval2  38082  cvrnbtwn2  38083  ishlat2  38161  3dim0  38266  islvol5  38388  pmapjat1  38662  pclcmpatN  38710  pclfinclN  38759  cdlemefrs29pre00  39204  cdlemefrs29bpre0  39205  cdlemefrs29cpre1  39207  cdleme32a  39250  cdlemftr3  39374  dvhopellsm  39926  dibelval3  39956  diblsmopel  39980  mapdvalc  40438  mapdval4N  40441  mapdordlem1a  40443  3factsumint2  40825  3factsumint3  40826  3factsumint4  40827  3factsumint  40828  aks4d1p8  40890  fsuppind  41112  diophrex  41446  rmxdioph  41688  dford4  41701  islmodfg  41744  islssfg2  41746  isdomn3  41879  fgraphopab  41885  cantnftermord  42003  tfsconcatlem  42019  naddsuc2  42076  k0004lem1  42831  ismnuprim  42986  2sbc5g  43108  limcrecl  44280  dvnmul  44594  dvnprodlem2  44598  fourierdlem83  44840  iundjiun  45111  fcoresf1ob  45718  f1ocof1ob  45724  4an21  45913  sprvalpwn0  46086  pairreueq  46113  prprsprreu  46122  prprreueq  46123  isrnghm  46624  isrnghmmul  46625  rngcinv  46781  rngcinvALTV  46793  ringcinv  46832  ringcinvALTV  46856  mpomptx2  46912  opnneir  47441  opnneilv  47443  i0oii  47454  io1ii  47455  iscnrm3lem3  47470