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  3532  spc2ed  3592  ceqsrex2v  3647  rexrab  3693  rexrab2  3697  reurab  3698  2reu5  3755  rexss  4056  inass  4220  rexin  4240  indifdirOLD  4286  difin2  4292  difrab  4309  reupick3  4320  inssdif0  4370  rexdifpr  4662  rexdifsn  4798  reusv2lem4  5400  reusv2  5402  eqvinop  5488  copsexgw  5491  copsexg  5492  rabxp  5725  elvvv  5752  resopab2  6037  difxp  6164  mptpreima  6238  resco  6250  coass  6265  dfpo2  6296  frpoind  6344  wfiOLD  6353  imadif  6633  dff1o2  6839  eqfnfv3  7035  f1ossf1o  7126  isoini  7335  f1oiso  7348  riotarab  7408  oprabidw  7440  oprabid  7441  dfoprab2  7467  mpoeq123  7481  mpomptx  7521  resoprab2  7527  ov3  7570  uniuni  7749  elxp4  7913  elxp5  7914  oprabex3  7964  frxp  8112  rexsupp  8167  brtpos2  8217  oeeui  8602  oeeu  8603  omabs  8650  eldifsucnn  8663  mapsnend  9036  xpsnen  9055  xpcomco  9062  xpassen  9066  wemapsolem  9545  epfrs  9726  frind  9745  aceq1  10112  dfac5lem1  10118  dfac5lem2  10119  dfac5lem5  10122  kmlem3  10147  kmlem14  10158  pwfseqlem1  10653  ltexpi  10897  ltexprlem4  11034  axaddf  11140  axmulf  11141  rexuz  12882  rexuz2  12883  nnwos  12899  zmin  12928  rexrp  12995  elixx3g  13337  elfz2  13491  preduz  13623  fzind2  13750  hashbclem  14411  resqrex  15197  rlim  15439  divalglem10  16345  divalgb  16347  gcdass  16489  lcmass  16551  isprm2  16619  infpn2  16846  ispos2  18268  issubmndb  18686  issubg3  19024  resscntz  19197  subgdmdprd  19904  dprd2d2  19914  dfrhm2  20253  aspval2  21452  fvmptnn04if  22351  ntreq0  22581  cmpcov2  22894  llyi  22978  nllyi  22979  ptpjpre1  23075  tx1cn  23113  tx2cn  23114  txtube  23144  txkgen  23156  trfil2  23391  elflim2  23468  cnpflfi  23503  isfcls  23513  cnextcn  23571  istlm  23689  blres  23937  metrest  24033  isnlm  24192  elpi1  24561  isclmp  24613  iscvsp  24644  isncvsngp  24666  iscph  24687  cfilucfil3  24837  itg1climres  25232  itgsubst  25566  ulmdvlem3  25914  cubic  26354  vmasum  26719  lgsquadlem1  26883  lgsquadlem2  26884  sltval2  27159  madeval2  27348  legov  27836  perpln1  27961  axcontlem5  28226  nbgrel  28597  nbusgredgeu0  28625  nb3grpr2  28640  finsumvtxdg2ssteplem3  28804  usgr2pth0  29022  isclwlke  29034  wwlksnfi  29160  elwwlks2ons3  29209  wpthswwlks2on  29215  usgr2wspthon  29219  rusgrnumwwlkl1  29222  isclwwlk  29237  isclwwlknx  29289  clwlknf1oclwwlkn  29337  clwwlknonel  29348  clwwlknon2x  29356  clwwlkvbij  29366  iseupthf1o  29455  fusgr2wsp2nb  29587  grpoidinvlem3  29759  h2hlm  30233  issh  30461  issh3  30472  ocsh  30536  cvbr2  31536  cvnbtwn2  31540  mdsl2i  31575  cvmdi  31577  mdsymlem2  31657  sumdmdii  31668  dmrab  31737  difrab2  31738  disjunsn  31825  mpomptxf  31905  ressupprn  31912  1stpreima  31928  2ndpreima  31929  f1od2  31946  nndiffz1  31997  omndmul2  32230  smatrcl  32776  crefdf  32828  1stmbfm  33259  2ndmbfm  33260  dya2iocnei  33281  eulerpartlemgvv  33375  eulerpartlemn  33380  bnj250  33712  bnj251  33713  bnj256  33717  bnj168  33741  cusgr3cyclex  34127  iscvm  34250  axacprim  34676  dfdm5  34744  dfrn5  34745  elima4  34747  dfon3  34864  brimg  34909  dfrecs2  34922  dfrdg4  34923  ifscgr  35016  cgrxfr  35027  segcon2  35077  seglecgr12im  35082  segletr  35086  ellines  35124  neifg  35256  bj-dfmpoa  35999  bj-imdiridlem  36066  bj-imdirco  36071  topdifinffinlem  36228  icorempo  36232  difunieq  36255  finxpreclem6  36277  wl-df4-3mintru2  36368  wl-cases2-dnf  36381  curf  36466  uncf  36467  matunitlindflem2  36485  matunitlindf  36486  poimirlem26  36514  poimirlem28  36516  poimirlem30  36518  poimirlem32  36520  poimir  36521  itg2addnc  36542  ftc1anclem5  36565  ftc1anc  36569  areacirclem5  36580  isbnd2  36651  heibor1  36678  anan  37093  br1cnvres  37137  inxpxrn  37265  prtlem70  37727  prtlem100  37729  lsateln0  37865  islshpat  37887  lcvbr2  37892  lcvnbtwn2  37897  isopos  38050  cvrval2  38144  cvrnbtwn2  38145  ishlat2  38223  3dim0  38328  islvol5  38450  pmapjat1  38724  pclcmpatN  38772  pclfinclN  38821  cdlemefrs29pre00  39266  cdlemefrs29bpre0  39267  cdlemefrs29cpre1  39269  cdleme32a  39312  cdlemftr3  39436  dvhopellsm  39988  dibelval3  40018  diblsmopel  40042  mapdvalc  40500  mapdval4N  40503  mapdordlem1a  40505  3factsumint2  40887  3factsumint3  40888  3factsumint4  40889  3factsumint  40890  aks4d1p8  40952  fsuppind  41162  diophrex  41513  rmxdioph  41755  dford4  41768  islmodfg  41811  islssfg2  41813  isdomn3  41946  fgraphopab  41952  cantnftermord  42070  tfsconcatlem  42086  naddsuc2  42143  k0004lem1  42898  ismnuprim  43053  2sbc5g  43175  limcrecl  44345  dvnmul  44659  dvnprodlem2  44663  fourierdlem83  44905  iundjiun  45176  fcoresf1ob  45783  f1ocof1ob  45789  4an21  45978  sprvalpwn0  46151  pairreueq  46178  prprsprreu  46187  prprreueq  46188  isrnghm  46690  isrnghmmul  46691  rngcinv  46879  rngcinvALTV  46891  ringcinv  46930  ringcinvALTV  46954  mpomptx2  47010  opnneir  47539  opnneilv  47541  i0oii  47552  io1ii  47553  iscnrm3lem3  47568