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

Syntax hints:   ↔ wb 208   ∧ 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 209  df-an 398

This theorem is referenced by:  bianass  649  an31  655  an4  663  3anass  1101  3an4anass  1111  4anpull2  1369  an33rean  1492  2sb5  2291  r19.41v  3171  r3ex  3180  r19.41  3245  rabrabi  3412  rabrab  3417  ceqsex3v  3486  spc2ed  3541  ceqsrex2v  3598  rexrab  3639  rexrab2  3643  reurab  3644  2reu5  3701  rexssOLD  3993  inass  4159  rexin  4181  difin2  4232  difrab  4249  reupick3  4261  inssdif0  4305  rabsneq  4577  rexdifpr  4594  rexdifsn  4730  reusv2lem4  5333  reusv2  5335  eqvinop  5430  copsexgw  5433  copsexgwOLD  5434  copsexg  5435  rabxp  5669  elvvv  5697  resopab2  5995  difxp  6119  mptpreima  6193  resco  6205  coass  6221  dfpo2  6251  frpoind  6297  imadif  6573  dff1o2  6776  eqfnfv3  6977  f1ossf1o  7074  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  9647  frind  9669  aceq1  10034  dfac5lem1  10040  dfac5lem2  10041  dfac5lem5  10044  kmlem3  10070  kmlem14  10081  pwfseqlem1  10576  ltexpi  10820  ltexprlem4  10957  axaddf  11063  axmulf  11064  rexuz  12843  rexuz2  12844  nnwos  12860  zmin  12889  rexrp  12960  elixx3g  13306  elfz2  13463  preduz  13599  fzind2  13738  hashbclem  14409  resqrex  15207  rlim  15452  divalglem10  16366  divalgb  16368  gcdass  16511  lcmass  16578  isprm2  16646  infpn2  16879  ispos2  18276  issubmndb  18768  issubg3  19115  resscntz  19303  subgdmdprd  20006  dprd2d2  20016  omndmul2  20103  isrnghm  20416  isrnghmmul  20417  dfrhm2  20449  rngcinv  20613  ringcinv  20647  isdomn3  20691  aspval2  21877  fvmptnn04if  22836  ntreq0  23064  cmpcov2  23377  llyi  23461  nllyi  23462  ptpjpre1  23558  tx1cn  23596  tx2cn  23597  txtube  23627  txkgen  23639  trfil2  23874  elflim2  23951  cnpflfi  23986  isfcls  23996  cnextcn  24054  istlm  24172  blres  24418  metrest  24511  isnlm  24662  elpi1  25034  isclmp  25086  iscvsp  25117  isncvsngp  25138  iscph  25159  cfilucfil3  25309  itg1climres  25703  itgsubst  26038  ulmdvlem3  26389  cubic  26835  vmasum  27201  lgsquadlem1  27365  lgsquadlem2  27366  ltsval2  27642  madeval2  27847  legov  28675  perpln1  28800  axcontlem5  29059  nbgrel  29431  nbusgredgeu0  29459  nb3grpr2  29474  finsumvtxdg2ssteplem3  29638  usgr2pth0  29855  isclwlke  29867  wwlksnfi  29996  elwwlks2ons3  30045  wpthswwlks2on  30054  usgr2wspthon  30058  rusgrnumwwlkl1  30061  isclwwlk  30076  isclwwlknx  30128  clwlknf1oclwwlkn  30176  clwwlknonel  30187  clwwlknon2x  30195  clwwlkvbij  30205  iseupthf1o  30294  fusgr2wsp2nb  30426  grpoidinvlem3  30599  h2hlm  31073  issh  31301  issh3  31312  ocsh  31376  cvbr2  32376  cvnbtwn2  32380  mdsl2i  32415  cvmdi  32417  mdsymlem2  32497  sumdmdii  32508  dmrab  32588  difrab2  32589  disjunsn  32687  mpomptxf  32774  ressupprn  32786  1stpreima  32803  2ndpreima  32804  f1od2  32815  nndiffz1  32882  1arithufdlem4  33642  r1plmhm  33705  r1pquslmic  33706  extdgfialglem1  33888  smatrcl  33992  crefdf  34044  1stmbfm  34456  2ndmbfm  34457  dya2iocnei  34478  eulerpartlemgvv  34572  eulerpartlemn  34577  bnj250  34899  bnj251  34900  bnj256  34904  bnj168  34928  cusgr3cyclex  35379  iscvm  35502  axacprim  35950  dfdm5  36016  dfrn5  36017  elima4  36019  dfon3  36133  brimg  36178  dfrecs2  36193  dfrdg4  36194  ifscgr  36287  cgrxfr  36298  segcon2  36348  seglecgr12im  36353  segletr  36357  ellines  36395  neifg  36614  bj-axseprep  37442  bj-dfmpoa  37491  bj-imdiridlem  37560  bj-imdirco  37565  topdifinffinlem  37724  icorempo  37728  difunieq  37751  finxpreclem6  37773  wl-df4-3mintru2  37864  wl-cases2-dnf  37898  curf  37980  uncf  37981  matunitlindflem2  37999  matunitlindf  38000  poimirlem26  38028  poimirlem28  38030  poimirlem30  38032  poimirlem32  38034  poimir  38035  itg2addnc  38056  ftc1anclem5  38079  ftc1anc  38083  areacirclem5  38094  isbnd2  38165  heibor1  38192  anan  38617  br1cnvres  38656  inxpxrn  38800  prtlem70  39364  prtlem100  39366  lsateln0  39502  islshpat  39524  lcvbr2  39529  lcvnbtwn2  39534  isopos  39687  cvrval2  39781  cvrnbtwn2  39782  ishlat2  39860  3dim0  39964  islvol5  40086  pmapjat1  40360  pclcmpatN  40408  pclfinclN  40457  cdlemefrs29pre00  40902  cdlemefrs29bpre0  40903  cdlemefrs29cpre1  40905  cdleme32a  40948  cdlemftr3  41072  dvhopellsm  41624  dibelval3  41654  diblsmopel  41678  mapdvalc  42136  mapdval4N  42139  mapdordlem1a  42141  3factsumint2  42522  3factsumint3  42523  3factsumint4  42524  3factsumint  42525  aks4d1p8  42587  redvmptabs  42852  fimgmcyc  43035  fsuppind  43055  diophrex  43239  rmxdioph  43476  dford4  43489  islmodfg  43529  islssfg2  43531  fgraphopab  43663  cantnftermord  43780  tfsconcatlem  43796  k0004lem1  44606  ismnuprim  44753  2sbc5g  44875  modelaxreplem3  45439  limcrecl  46088  dvnmul  46400  dvnprodlem2  46404  fourierdlem83  46646  iundjiun  46917  fcoresf1ob  47550  f1ocof1ob  47558  4an21  47747  sprvalpwn0  47972  pairreueq  47999  prprsprreu  48008  prprreueq  48009  clnbgrel  48333  dfvopnbgr2  48358  rngcinvALTV  48781  ringcinvALTV  48815  mpomptx2  48840  reuxfr1dd  49311  coxp  49337  opnneir  49411  opnneilv  49413  i0oii  49424  io1ii  49425  upfval2  49681