Theorem anass 469

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

Syntax hints:   ↔ wb 205   ∧ wa 396

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 397

This theorem is referenced by:  bianass  639  an31  645  an4  653  3anass  1094  3an4anass  1104  an33rean  1482  2sb5  2272  r19.41v  3276  r19.41  3277  rabrab  3311  rabrabi  3427  ceqsex3v  3484  spc2ed  3540  ceqsrex2v  3587  rexrab  3633  rexrab2  3637  2reu5  3693  rexss  3992  inass  4153  rexin  4173  indifdirOLD  4219  difin2  4225  difrab  4242  reupick3  4253  inssdif0  4303  rexdifpr  4594  rexdifsn  4727  reusv2lem4  5324  reusv2  5326  eqvinop  5401  copsexgw  5404  copsexg  5405  rabxp  5635  elvvv  5662  resopab2  5944  difxp  6067  mptpreima  6141  resco  6154  coass  6169  dfpo2  6199  frpoind  6245  wfiOLD  6254  imadif  6518  dff1o2  6721  eqfnfv3  6911  f1ossf1o  7000  isoini  7209  f1oiso  7222  oprabidw  7306  oprabid  7307  dfoprab2  7333  mpoeq123  7347  mpomptx  7387  resoprab2  7393  ov3  7435  uniuni  7612  elxp4  7769  elxp5  7770  oprabex3  7820  frxp  7967  rexsupp  7998  brtpos2  8048  oeeui  8433  oeeu  8434  omabs  8481  eldifsucnn  8494  mapsnend  8826  xpsnen  8842  xpcomco  8849  xpassen  8853  wemapsolem  9309  epfrs  9489  frind  9508  aceq1  9873  dfac5lem1  9879  dfac5lem2  9880  dfac5lem5  9883  kmlem3  9908  kmlem14  9919  pwfseqlem1  10414  ltexpi  10658  ltexprlem4  10795  axaddf  10901  axmulf  10902  rexuz  12638  rexuz2  12639  nnwos  12655  zmin  12684  rexrp  12751  elixx3g  13092  elfz2  13246  preduz  13378  fzind2  13505  hashbclem  14164  resqrex  14962  rlim  15204  divalglem10  16111  divalgb  16113  gcdass  16255  lcmass  16319  isprm2  16387  infpn2  16614  ispos2  18033  issubmndb  18444  issubg3  18773  resscntz  18938  subgdmdprd  19637  dprd2d2  19647  dfrhm2  19961  isassa  21063  aspval2  21102  fvmptnn04if  21998  ntreq0  22228  cmpcov2  22541  llyi  22625  nllyi  22626  ptpjpre1  22722  tx1cn  22760  tx2cn  22761  txtube  22791  txkgen  22803  trfil2  23038  elflim2  23115  cnpflfi  23150  isfcls  23160  cnextcn  23218  istlm  23336  blres  23584  metrest  23680  isnlm  23839  elpi1  24208  isclmp  24260  iscvsp  24291  isncvsngp  24313  iscph  24334  cfilucfil3  24484  itg1climres  24879  itgsubst  25213  ulmdvlem3  25561  cubic  25999  vmasum  26364  lgsquadlem1  26528  lgsquadlem2  26529  legov  26946  perpln1  27071  axcontlem5  27336  nbgrel  27707  nbusgredgeu0  27735  nb3grpr2  27750  finsumvtxdg2ssteplem3  27914  usgr2pth0  28133  isclwlke  28145  wwlksnfi  28271  elwwlks2ons3  28320  wpthswwlks2on  28326  usgr2wspthon  28330  rusgrnumwwlkl1  28333  isclwwlk  28348  isclwwlknx  28400  clwlknf1oclwwlkn  28448  clwwlknonel  28459  clwwlknon2x  28467  clwwlkvbij  28477  iseupthf1o  28566  fusgr2wsp2nb  28698  grpoidinvlem3  28868  h2hlm  29342  issh  29570  issh3  29581  ocsh  29645  cvbr2  30645  cvnbtwn2  30649  mdsl2i  30684  cvmdi  30686  mdsymlem2  30766  sumdmdii  30777  dmrab  30844  difrab2  30845  disjunsn  30933  mpomptxf  31016  ressupprn  31024  1stpreima  31039  2ndpreima  31040  f1od2  31056  nndiffz1  31107  omndmul2  31338  smatrcl  31746  crefdf  31798  1stmbfm  32227  2ndmbfm  32228  dya2iocnei  32249  eulerpartlemgvv  32343  eulerpartlemn  32348  bnj250  32680  bnj251  32681  bnj256  32685  bnj168  32709  cusgr3cyclex  33098  iscvm  33221  axacprim  33648  riotarab  33673  reurab  33674  dfdm5  33747  dfrn5  33748  elima4  33750  sltval2  33859  madeval2  34037  dfon3  34194  brimg  34239  dfrecs2  34252  dfrdg4  34253  ifscgr  34346  cgrxfr  34357  segcon2  34407  seglecgr12im  34412  segletr  34416  ellines  34454  neifg  34560  bj-dfmpoa  35289  bj-imdiridlem  35356  bj-imdirco  35361  topdifinffinlem  35518  icorempo  35522  difunieq  35545  finxpreclem6  35567  wl-df4-3mintru2  35658  wl-cases2-dnf  35671  curf  35755  uncf  35756  matunitlindflem2  35774  matunitlindf  35775  poimirlem26  35803  poimirlem28  35805  poimirlem30  35807  poimirlem32  35809  poimir  35810  itg2addnc  35831  ftc1anclem5  35854  ftc1anc  35858  areacirclem5  35869  isbnd2  35941  heibor1  35968  anan  36379  inxpxrn  36521  prtlem70  36871  prtlem100  36873  lsateln0  37009  islshpat  37031  lcvbr2  37036  lcvnbtwn2  37041  isopos  37194  cvrval2  37288  cvrnbtwn2  37289  ishlat2  37367  3dim0  37471  islvol5  37593  pmapjat1  37867  pclcmpatN  37915  pclfinclN  37964  cdlemefrs29pre00  38409  cdlemefrs29bpre0  38410  cdlemefrs29cpre1  38412  cdleme32a  38455  cdlemftr3  38579  dvhopellsm  39131  dibelval3  39161  diblsmopel  39185  mapdvalc  39643  mapdval4N  39646  mapdordlem1a  39648  3factsumint2  40030  3factsumint3  40031  3factsumint4  40032  3factsumint  40033  aks4d1p8  40095  fsuppind  40279  diophrex  40597  rmxdioph  40838  dford4  40851  islmodfg  40894  islssfg2  40896  isdomn3  41029  fgraphopab  41035  k0004lem1  41757  ismnuprim  41912  2sbc5g  42034  limcrecl  43170  dvnmul  43484  dvnprodlem2  43488  fourierdlem83  43730  iundjiun  43998  fcoresf1ob  44567  f1ocof1ob  44573  4an21  44762  sprvalpwn0  44935  pairreueq  44962  prprsprreu  44971  prprreueq  44972  isrnghm  45450  isrnghmmul  45451  rngcinv  45539  rngcinvALTV  45551  ringcinv  45590  ringcinvALTV  45614  mpomptx2  45670  opnneir  46200  opnneilv  46202  i0oii  46213  io1ii  46214  iscnrm3lem3  46229