Theorem anass 474

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 23	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
2	1	anassrs 473	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		id 23	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	anasss 472	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	2, 4	impbii 212	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bianass  655  an31  661  an4  669  3anass  1111  3an4anass  1122  4anpull2OLD  1383  an33rean  1514  2sb5  2311  r19.41v  3192  r3ex  3201  r19.41  3266  rabrabi  3430  rabrab  3435  ceqsex3v  3502  spc2ed  3555  ceqsrex2v  3612  rexrab  3654  rexrab2  3658  reurab  3659  2reu5  3716  rexssOLD  4007  inass  4173  rexin  4196  difin2  4247  difrab  4264  reupick3  4276  inssdif0OLD  4323  rabsneq  4603  rexdifpr  4620  rexdifsn  4757  reusv2lem4  5366  reusv2  5368  eqvinop  5463  copsexgw  5466  copsexgwOLD  5467  copsexg  5468  rabxp  5703  elvvv  5731  resopab2  6033  difxp  6157  mptpreima  6235  resco  6247  coass  6263  dfpo2  6295  frpoind  6341  imadif  6619  dff1o2  6825  eqfnfv3  7026  f1ossf1o  7124  isoini  7341  f1oiso  7354  riotarab  7414  oprabidw  7446  oprabid  7447  dfoprab2  7473  mpoeq123  7487  mpomptx  7528  resoprab2  7534  ov3  7578  uniuni  7763  elxp4  7921  elxp5  7922  oprabex3  7976  frxp  8126  rexsupp  8182  brtpos2  8232  oeeui  8594  oeeu  8595  omabs  8643  eldifsucnn  8656  naddsuc2  8694  curf  8873  uncf  8874  mapsnend  9047  xpsnen  9063  xpcomco  9069  xpassen  9073  wemapsolem  9526  epfrs  9714  frind  9736  aceq1  10142  dfac5lem1  10148  dfac5lem2  10149  dfac5lem5  10152  kmlem3  10177  kmlem14  10188  pwfseqlem1  10689  ltexpi  10933  ltexprlem4  11070  axaddf  11176  axmulf  11177  rexuz  12969  rexuz2  12970  nnwos  12986  zmin  13015  rexrp  13087  elixx3g  13433  elfz2  13590  preduz  13727  fzind2  13866  hashbclem  14539  resqrex  15359  rlim  15604  divalglem10  16514  divalgb  16516  gcdass  16659  lcmass  16726  isprm2  16794  infpn2  17027  ispos2  18425  issubmndb  18936  issubg3  19291  resscntz  19483  subgdmdprd  20186  dprd2d2  20196  omndmul2  20283  dfring3  20454  isrnghm  20607  isrnghmmul  20608  dfrhm2  20640  rngcinv  20825  ringcinv  20859  isdomn3  20902  aspval2  22142  matunitlindflem2  22931  matunitlindf  22932  fvmptnn04if  23103  ntreq0  23331  cmpcov2  23644  llyi  23729  nllyi  23730  ptpjpre1  23826  tx1cn  23864  tx2cn  23865  txtube  23895  txkgen  23907  trfil2  24142  elflim2  24219  cnpflfi  24254  isfcls  24264  cnextcn  24322  istlm  24440  blres  24686  metrest  24779  isnlm  24930  elpi1  25302  isclmp  25354  iscvsp  25385  isncvsngp  25406  iscph  25427  cfilucfil3  25577  itg1climres  25971  itgsubst  26305  ulmdvlem3  26667  cubic  27115  vmasum  27481  lgsquadlem1  27645  lgsquadlem2  27646  ltsval2  27921  madeval2  28127  legov  28956  perpln1  29093  prlngmolem2  29339  axcontlem5  29454  nbgrel  29829  nbusgredgeu0  29857  nb3grpr2  29872  finsumvtxdg2ssteplem3  30036  usgr2pth0  30259  isclwlke  30272  wwlksnfi  30403  elwwlks2ons3  30452  wpthswwlks2on  30461  usgr2wspthon  30465  rusgrnumwwlkl1  30468  isclwwlk  30483  isclwwlknx  30535  clwlknf1oclwwlkn  30583  clwwlknonel  30594  clwwlknon2x  30602  clwwlkvbij  30612  iseupthf1o  30711  fusgr2wsp2nb  30843  grpoidinvlem3  31016  h2hlm  31490  issh  31718  issh3  31729  ocsh  31793  cvbr2  32793  cvnbtwn2  32797  mdsl2i  32832  cvmdi  32834  mdsymlem2  32914  sumdmdii  32925  dmrab  33001  difrab2  33002  disjunsn  33096  mpomptxf  33180  ressupprn  33191  1stpreima  33208  2ndpreima  33209  f1od2  33219  nndiffz1  33286  1arithufdlem4  33987  r1plmhm  34049  r1pquslmic  34050  extdgfialglem1  34232  smatrcl  34336  crefdf  34388  1stmbfm  34801  2ndmbfm  34802  dya2iocnei  34823  eulerpartlemgvv  34917  eulerpartlemn  34922  bnj250  35241  bnj251  35242  bnj256  35246  bnj168  35270  cusgr3cyclex  35755  iscvm  35868  axacprim  36316  dfdm5  36382  dfrn5  36383  elima4  36385  dfon3  36499  brimg  36544  dfrecs2  36559  dfrdg4  36560  ifscgr  36654  cgrxfr  36665  segcon2  36715  seglecgr12im  36720  segletr  36724  ellines  36762  neifg  37004  bj-axseprep  37833  bj-dfmpoa  37882  bj-imdiridlem  37951  bj-imdirco  37956  topdifinffinlem  38115  icorempo  38119  difunieq  38142  finxpreclem6  38164  wl-df4-3mintru2  38255  wl-cases2-dnf  38289  poimirlem26  38409  poimirlem28  38411  poimirlem30  38413  poimirlem32  38415  poimir  38416  itg2addnc  38437  ftc1anclem5  38460  ftc1anc  38464  areacirclem5  38475  isbnd2  38547  heibor1  38574  anan  38997  br1cnvres  39036  inxpxrn  39180  prtlem70  39744  prtlem100  39746  lsateln0  39882  islshpat  39904  lcvbr2  39909  lcvnbtwn2  39914  isopos  40067  cvrval2  40161  cvrnbtwn2  40162  ishlat2  40240  3dim0  40344  islvol5  40466  pmapjat1  40740  pclcmpatN  40788  pclfinclN  40837  cdlemefrs29pre00  41282  cdlemefrs29bpre0  41283  cdlemefrs29cpre1  41285  cdleme32a  41328  cdlemftr3  41452  dvhopellsm  42004  dibelval3  42034  diblsmopel  42058  mapdvalc  42516  mapdval4N  42519  mapdordlem1a  42521  3factsumint2  42902  3factsumint3  42903  3factsumint4  42904  3factsumint  42905  aks4d1p8  42967  redvmptabs  43249  fimgmcyc  43430  fsuppind  43450  diophrex  43634  rmxdioph  43871  dford4  43884  islmodfg  43924  islssfg2  43926  fgraphopab  44058  cantnftermord  44175  tfsconcatlem  44191  k0004lem1  45001  ismnuprim  45132  2sbc5g  45254  modelaxreplem3  45817  limcrecl  46473  dvnmul  46785  dvnprodlem2  46789  fourierdlem83  47031  iundjiun  47302  fcoresf1ob  47975  f1ocof1ob  47983  4an21  48172  sprvalpwn0  48397  pairreueq  48424  prprsprreu  48433  prprreueq  48434  clnbgrel  48758  dfvopnbgr2  48783  rngcinvALTV  49205  ringcinvALTV  49239  mpomptx2  49279  reuxfr1dd  49749  coxp  49775  opnneir  49847  opnneilv  49849  i0oii  49860  io1ii  49861  upfval2  50117  alsanmo  50753  ralsanmo  50754  2alsraln0  50760