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  643  an31  649  an4  657  3anass  1095  3an4anass  1105  4anpull2  1363  an33rean  1486  2sb5  2285  r19.41v  3167  r3ex  3176  r19.41  3241  rabrabi  3419  rabrab  3424  ceqsex3v  3496  spc2ed  3556  ceqsrex2v  3613  rexrab  3655  rexrab2  3659  reurab  3660  2reu5  3717  rexssOLD  4012  inass  4181  rexin  4203  difin2  4254  difrab  4271  reupick3  4283  inssdif0  4327  rabsneq  4600  rexdifpr  4617  rexdifsn  4751  reusv2lem4  5347  reusv2  5349  eqvinop  5436  copsexgw  5439  copsexg  5440  rabxp  5673  elvvv  5701  resopab2  5996  difxp  6123  mptpreima  6197  resco  6209  coass  6225  dfpo2  6255  frpoind  6301  imadif  6577  dff1o2  6780  eqfnfv3  6980  f1ossf1o  7075  isoini  7286  f1oiso  7299  riotarab  7359  oprabidw  7391  oprabid  7392  dfoprab2  7418  mpoeq123  7432  mpomptx  7473  resoprab2  7479  ov3  7523  uniuni  7709  elxp4  7866  elxp5  7867  oprabex3  7923  frxp  8070  rexsupp  8126  brtpos2  8176  oeeui  8532  oeeu  8533  omabs  8581  eldifsucnn  8594  naddsuc2  8631  mapsnend  8977  xpsnen  8993  xpcomco  8999  xpassen  9003  wemapsolem  9459  epfrs  9644  frind  9666  aceq1  10031  dfac5lem1  10037  dfac5lem2  10038  dfac5lem5  10041  kmlem3  10067  kmlem14  10078  pwfseqlem1  10573  ltexpi  10817  ltexprlem4  10954  axaddf  11060  axmulf  11061  rexuz  12815  rexuz2  12816  nnwos  12832  zmin  12861  rexrp  12932  elixx3g  13278  elfz2  13434  preduz  13570  fzind2  13708  hashbclem  14379  resqrex  15177  rlim  15422  divalglem10  16333  divalgb  16335  gcdass  16478  lcmass  16545  isprm2  16613  infpn2  16845  ispos2  18242  issubmndb  18734  issubg3  19078  resscntz  19266  subgdmdprd  19969  dprd2d2  19979  omndmul2  20066  isrnghm  20381  isrnghmmul  20382  dfrhm2  20414  rngcinv  20574  ringcinv  20608  isdomn3  20652  aspval2  21858  fvmptnn04if  22797  ntreq0  23025  cmpcov2  23338  llyi  23422  nllyi  23423  ptpjpre1  23519  tx1cn  23557  tx2cn  23558  txtube  23588  txkgen  23600  trfil2  23835  elflim2  23912  cnpflfi  23947  isfcls  23957  cnextcn  24015  istlm  24133  blres  24379  metrest  24472  isnlm  24623  elpi1  25005  isclmp  25057  iscvsp  25088  isncvsngp  25109  iscph  25130  cfilucfil3  25280  itg1climres  25675  itgsubst  26016  ulmdvlem3  26371  cubic  26819  vmasum  27187  lgsquadlem1  27351  lgsquadlem2  27352  ltsval2  27628  madeval2  27833  legov  28661  perpln1  28786  axcontlem5  29045  nbgrel  29417  nbusgredgeu0  29445  nb3grpr2  29460  finsumvtxdg2ssteplem3  29625  usgr2pth0  29842  isclwlke  29854  wwlksnfi  29983  elwwlks2ons3  30032  wpthswwlks2on  30041  usgr2wspthon  30045  rusgrnumwwlkl1  30048  isclwwlk  30063  isclwwlknx  30115  clwlknf1oclwwlkn  30163  clwwlknonel  30174  clwwlknon2x  30182  clwwlkvbij  30192  iseupthf1o  30281  fusgr2wsp2nb  30413  grpoidinvlem3  30585  h2hlm  31059  issh  31287  issh3  31298  ocsh  31362  cvbr2  32362  cvnbtwn2  32366  mdsl2i  32401  cvmdi  32403  mdsymlem2  32483  sumdmdii  32494  dmrab  32574  difrab2  32575  disjunsn  32672  mpomptxf  32759  ressupprn  32771  1stpreima  32788  2ndpreima  32789  f1od2  32800  nndiffz1  32868  1arithufdlem4  33630  r1plmhm  33693  r1pquslmic  33694  extdgfialglem1  33851  smatrcl  33955  crefdf  34007  1stmbfm  34419  2ndmbfm  34420  dya2iocnei  34441  eulerpartlemgvv  34535  eulerpartlemn  34540  bnj250  34859  bnj251  34860  bnj256  34864  bnj168  34888  cusgr3cyclex  35332  iscvm  35455  axacprim  35903  dfdm5  35969  dfrn5  35970  elima4  35972  dfon3  36086  brimg  36131  dfrecs2  36146  dfrdg4  36147  ifscgr  36240  cgrxfr  36251  segcon2  36301  seglecgr12im  36306  segletr  36310  ellines  36348  neifg  36567  bj-dfmpoa  37325  bj-imdiridlem  37392  bj-imdirco  37397  topdifinffinlem  37554  icorempo  37558  difunieq  37581  finxpreclem6  37603  wl-df4-3mintru2  37694  wl-cases2-dnf  37719  curf  37801  uncf  37802  matunitlindflem2  37820  matunitlindf  37821  poimirlem26  37849  poimirlem28  37851  poimirlem30  37853  poimirlem32  37855  poimir  37856  itg2addnc  37877  ftc1anclem5  37900  ftc1anc  37904  areacirclem5  37915  isbnd2  37986  heibor1  38013  anan  38438  br1cnvres  38477  inxpxrn  38621  prtlem70  39185  prtlem100  39187  lsateln0  39323  islshpat  39345  lcvbr2  39350  lcvnbtwn2  39355  isopos  39508  cvrval2  39602  cvrnbtwn2  39603  ishlat2  39681  3dim0  39785  islvol5  39907  pmapjat1  40181  pclcmpatN  40229  pclfinclN  40278  cdlemefrs29pre00  40723  cdlemefrs29bpre0  40724  cdlemefrs29cpre1  40726  cdleme32a  40769  cdlemftr3  40893  dvhopellsm  41445  dibelval3  41475  diblsmopel  41499  mapdvalc  41957  mapdval4N  41960  mapdordlem1a  41962  3factsumint2  42344  3factsumint3  42345  3factsumint4  42346  3factsumint  42347  aks4d1p8  42409  redvmptabs  42682  fimgmcyc  42856  fsuppind  42900  diophrex  43084  rmxdioph  43325  dford4  43338  islmodfg  43378  islssfg2  43380  fgraphopab  43512  cantnftermord  43629  tfsconcatlem  43645  k0004lem1  44455  ismnuprim  44602  2sbc5g  44724  modelaxreplem3  45288  limcrecl  45942  dvnmul  46254  dvnprodlem2  46258  fourierdlem83  46500  iundjiun  46771  fcoresf1ob  47386  f1ocof1ob  47394  4an21  47583  sprvalpwn0  47796  pairreueq  47823  prprsprreu  47832  prprreueq  47833  clnbgrel  48141  dfvopnbgr2  48166  rngcinvALTV  48589  ringcinvALTV  48623  mpomptx2  48648  reuxfr1dd  49119  coxp  49145  opnneir  49219  opnneilv  49221  i0oii  49232  io1ii  49233  upfval2  49489