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  642  an31  648  an4  656  3anass  1094  3an4anass  1104  4anpull2  1362  an33rean  1485  2sb5  2282  r19.41v  3164  r3ex  3173  r19.41  3238  rabrabi  3416  rabrab  3421  ceqsex3v  3493  spc2ed  3553  ceqsrex2v  3610  rexrab  3652  rexrab2  3656  reurab  3657  2reu5  3714  rexssOLD  4009  inass  4178  rexin  4200  difin2  4251  difrab  4268  reupick3  4280  inssdif0  4324  rabsneq  4597  rexdifpr  4614  rexdifsn  4748  reusv2lem4  5344  reusv2  5346  eqvinop  5433  copsexgw  5436  copsexg  5437  rabxp  5670  elvvv  5698  resopab2  5993  difxp  6120  mptpreima  6194  resco  6206  coass  6222  dfpo2  6252  frpoind  6298  imadif  6574  dff1o2  6777  eqfnfv3  6976  f1ossf1o  7071  isoini  7282  f1oiso  7295  riotarab  7355  oprabidw  7387  oprabid  7388  dfoprab2  7414  mpoeq123  7428  mpomptx  7469  resoprab2  7475  ov3  7519  uniuni  7705  elxp4  7862  elxp5  7863  oprabex3  7919  frxp  8066  rexsupp  8122  brtpos2  8172  oeeui  8528  oeeu  8529  omabs  8577  eldifsucnn  8590  naddsuc2  8627  mapsnend  8971  xpsnen  8987  xpcomco  8993  xpassen  8997  wemapsolem  9453  epfrs  9638  frind  9660  aceq1  10025  dfac5lem1  10031  dfac5lem2  10032  dfac5lem5  10035  kmlem3  10061  kmlem14  10072  pwfseqlem1  10567  ltexpi  10811  ltexprlem4  10948  axaddf  11054  axmulf  11055  rexuz  12809  rexuz2  12810  nnwos  12826  zmin  12855  rexrp  12926  elixx3g  13272  elfz2  13428  preduz  13564  fzind2  13702  hashbclem  14373  resqrex  15171  rlim  15416  divalglem10  16327  divalgb  16329  gcdass  16472  lcmass  16539  isprm2  16607  infpn2  16839  ispos2  18236  issubmndb  18728  issubg3  19072  resscntz  19260  subgdmdprd  19963  dprd2d2  19973  omndmul2  20060  isrnghm  20375  isrnghmmul  20376  dfrhm2  20408  rngcinv  20568  ringcinv  20602  isdomn3  20646  aspval2  21852  fvmptnn04if  22791  ntreq0  23019  cmpcov2  23332  llyi  23416  nllyi  23417  ptpjpre1  23513  tx1cn  23551  tx2cn  23552  txtube  23582  txkgen  23594  trfil2  23829  elflim2  23906  cnpflfi  23941  isfcls  23951  cnextcn  24009  istlm  24127  blres  24373  metrest  24466  isnlm  24617  elpi1  24999  isclmp  25051  iscvsp  25082  isncvsngp  25103  iscph  25124  cfilucfil3  25274  itg1climres  25669  itgsubst  26010  ulmdvlem3  26365  cubic  26813  vmasum  27181  lgsquadlem1  27345  lgsquadlem2  27346  sltval2  27622  madeval2  27821  legov  28606  perpln1  28731  axcontlem5  28990  nbgrel  29362  nbusgredgeu0  29390  nb3grpr2  29405  finsumvtxdg2ssteplem3  29570  usgr2pth0  29787  isclwlke  29799  wwlksnfi  29928  elwwlks2ons3  29977  wpthswwlks2on  29986  usgr2wspthon  29990  rusgrnumwwlkl1  29993  isclwwlk  30008  isclwwlknx  30060  clwlknf1oclwwlkn  30108  clwwlknonel  30119  clwwlknon2x  30127  clwwlkvbij  30137  iseupthf1o  30226  fusgr2wsp2nb  30358  grpoidinvlem3  30530  h2hlm  31004  issh  31232  issh3  31243  ocsh  31307  cvbr2  32307  cvnbtwn2  32311  mdsl2i  32346  cvmdi  32348  mdsymlem2  32428  sumdmdii  32439  dmrab  32520  difrab2  32521  disjunsn  32618  mpomptxf  32706  ressupprn  32718  1stpreima  32735  2ndpreima  32736  f1od2  32747  nndiffz1  32815  1arithufdlem4  33577  r1plmhm  33640  r1pquslmic  33641  extdgfialglem1  33798  smatrcl  33902  crefdf  33954  1stmbfm  34366  2ndmbfm  34367  dya2iocnei  34388  eulerpartlemgvv  34482  eulerpartlemn  34487  bnj250  34806  bnj251  34807  bnj256  34811  bnj168  34835  cusgr3cyclex  35279  iscvm  35402  axacprim  35850  dfdm5  35916  dfrn5  35917  elima4  35919  dfon3  36033  brimg  36078  dfrecs2  36093  dfrdg4  36094  ifscgr  36187  cgrxfr  36198  segcon2  36248  seglecgr12im  36253  segletr  36257  ellines  36295  neifg  36514  bj-dfmpoa  37262  bj-imdiridlem  37329  bj-imdirco  37334  topdifinffinlem  37491  icorempo  37495  difunieq  37518  finxpreclem6  37540  wl-df4-3mintru2  37631  wl-cases2-dnf  37656  curf  37738  uncf  37739  matunitlindflem2  37757  matunitlindf  37758  poimirlem26  37786  poimirlem28  37788  poimirlem30  37790  poimirlem32  37792  poimir  37793  itg2addnc  37814  ftc1anclem5  37837  ftc1anc  37841  areacirclem5  37852  isbnd2  37923  heibor1  37950  anan  38370  br1cnvres  38406  inxpxrn  38542  prtlem70  39056  prtlem100  39058  lsateln0  39194  islshpat  39216  lcvbr2  39221  lcvnbtwn2  39226  isopos  39379  cvrval2  39473  cvrnbtwn2  39474  ishlat2  39552  3dim0  39656  islvol5  39778  pmapjat1  40052  pclcmpatN  40100  pclfinclN  40149  cdlemefrs29pre00  40594  cdlemefrs29bpre0  40595  cdlemefrs29cpre1  40597  cdleme32a  40640  cdlemftr3  40764  dvhopellsm  41316  dibelval3  41346  diblsmopel  41370  mapdvalc  41828  mapdval4N  41831  mapdordlem1a  41833  3factsumint2  42215  3factsumint3  42216  3factsumint4  42217  3factsumint  42218  aks4d1p8  42280  redvmptabs  42557  fimgmcyc  42731  fsuppind  42775  diophrex  42959  rmxdioph  43200  dford4  43213  islmodfg  43253  islssfg2  43255  fgraphopab  43387  cantnftermord  43504  tfsconcatlem  43520  k0004lem1  44330  ismnuprim  44477  2sbc5g  44599  modelaxreplem3  45163  limcrecl  45817  dvnmul  46129  dvnprodlem2  46133  fourierdlem83  46375  iundjiun  46646  fcoresf1ob  47261  f1ocof1ob  47269  4an21  47458  sprvalpwn0  47671  pairreueq  47698  prprsprreu  47707  prprreueq  47708  clnbgrel  48016  dfvopnbgr2  48041  rngcinvALTV  48464  ringcinvALTV  48498  mpomptx2  48523  reuxfr1dd  48994  coxp  49020  opnneir  49094  opnneilv  49096  i0oii  49107  io1ii  49108  upfval2  49364