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  3168  r3ex  3177  r19.41  3242  rabrabi  3409  rabrab  3414  ceqsex3v  3484  spc2ed  3544  ceqsrex2v  3601  rexrab  3643  rexrab2  3647  reurab  3648  2reu5  3705  rexssOLD  4000  inass  4169  rexin  4191  difin2  4242  difrab  4259  reupick3  4271  inssdif0  4315  rabsneq  4587  rexdifpr  4604  rexdifsn  4738  reusv2lem4  5340  reusv2  5342  eqvinop  5437  copsexgw  5440  copsexg  5441  rabxp  5674  elvvv  5702  resopab2  5997  difxp  6124  mptpreima  6198  resco  6210  coass  6226  dfpo2  6256  frpoind  6302  imadif  6578  dff1o2  6781  eqfnfv3  6981  f1ossf1o  7077  isoini  7288  f1oiso  7301  riotarab  7361  oprabidw  7393  oprabid  7394  dfoprab2  7420  mpoeq123  7434  mpomptx  7475  resoprab2  7481  ov3  7525  uniuni  7711  elxp4  7868  elxp5  7869  oprabex3  7925  frxp  8071  rexsupp  8127  brtpos2  8177  oeeui  8533  oeeu  8534  omabs  8582  eldifsucnn  8595  naddsuc2  8632  mapsnend  8978  xpsnen  8994  xpcomco  9000  xpassen  9004  wemapsolem  9460  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  20609  ringcinv  20643  isdomn3  20687  aspval2  21892  fvmptnn04if  22828  ntreq0  23056  cmpcov2  23369  llyi  23453  nllyi  23454  ptpjpre1  23550  tx1cn  23588  tx2cn  23589  txtube  23619  txkgen  23631  trfil2  23866  elflim2  23943  cnpflfi  23978  isfcls  23988  cnextcn  24046  istlm  24164  blres  24410  metrest  24503  isnlm  24654  elpi1  25026  isclmp  25078  iscvsp  25109  isncvsngp  25130  iscph  25151  cfilucfil3  25301  itg1climres  25695  itgsubst  26030  ulmdvlem3  26384  cubic  26830  vmasum  27197  lgsquadlem1  27361  lgsquadlem2  27362  ltsval2  27638  madeval2  27843  legov  28671  perpln1  28796  axcontlem5  29055  nbgrel  29427  nbusgredgeu0  29455  nb3grpr2  29470  finsumvtxdg2ssteplem3  29635  usgr2pth0  29852  isclwlke  29864  wwlksnfi  29993  elwwlks2ons3  30042  wpthswwlks2on  30051  usgr2wspthon  30055  rusgrnumwwlkl1  30058  isclwwlk  30073  isclwwlknx  30125  clwlknf1oclwwlkn  30173  clwwlknonel  30184  clwwlknon2x  30192  clwwlkvbij  30202  iseupthf1o  30291  fusgr2wsp2nb  30423  grpoidinvlem3  30596  h2hlm  31070  issh  31298  issh3  31309  ocsh  31373  cvbr2  32373  cvnbtwn2  32377  mdsl2i  32412  cvmdi  32414  mdsymlem2  32494  sumdmdii  32505  dmrab  32585  difrab2  32586  disjunsn  32683  mpomptxf  32770  ressupprn  32782  1stpreima  32799  2ndpreima  32800  f1od2  32811  nndiffz1  32878  1arithufdlem4  33626  r1plmhm  33689  r1pquslmic  33690  extdgfialglem1  33856  smatrcl  33960  crefdf  34012  1stmbfm  34424  2ndmbfm  34425  dya2iocnei  34446  eulerpartlemgvv  34540  eulerpartlemn  34545  bnj250  34864  bnj251  34865  bnj256  34869  bnj168  34893  cusgr3cyclex  35338  iscvm  35461  axacprim  35909  dfdm5  35975  dfrn5  35976  elima4  35978  dfon3  36092  brimg  36137  dfrecs2  36152  dfrdg4  36153  ifscgr  36246  cgrxfr  36257  segcon2  36307  seglecgr12im  36312  segletr  36316  ellines  36354  neifg  36573  bj-axseprep  37401  bj-dfmpoa  37450  bj-imdiridlem  37519  bj-imdirco  37524  topdifinffinlem  37681  icorempo  37685  difunieq  37708  finxpreclem6  37730  wl-df4-3mintru2  37821  wl-cases2-dnf  37855  curf  37937  uncf  37938  matunitlindflem2  37956  matunitlindf  37957  poimirlem26  37985  poimirlem28  37987  poimirlem30  37989  poimirlem32  37991  poimir  37992  itg2addnc  38013  ftc1anclem5  38036  ftc1anc  38040  areacirclem5  38051  isbnd2  38122  heibor1  38149  anan  38574  br1cnvres  38613  inxpxrn  38757  prtlem70  39321  prtlem100  39323  lsateln0  39459  islshpat  39481  lcvbr2  39486  lcvnbtwn2  39491  isopos  39644  cvrval2  39738  cvrnbtwn2  39739  ishlat2  39817  3dim0  39921  islvol5  40043  pmapjat1  40317  pclcmpatN  40365  pclfinclN  40414  cdlemefrs29pre00  40859  cdlemefrs29bpre0  40860  cdlemefrs29cpre1  40862  cdleme32a  40905  cdlemftr3  41029  dvhopellsm  41581  dibelval3  41611  diblsmopel  41635  mapdvalc  42093  mapdval4N  42096  mapdordlem1a  42098  3factsumint2  42479  3factsumint3  42480  3factsumint4  42481  3factsumint  42482  aks4d1p8  42544  redvmptabs  42810  fimgmcyc  42997  fsuppind  43041  diophrex  43225  rmxdioph  43466  dford4  43479  islmodfg  43519  islssfg2  43521  fgraphopab  43653  cantnftermord  43770  tfsconcatlem  43786  k0004lem1  44596  ismnuprim  44743  2sbc5g  44865  modelaxreplem3  45429  limcrecl  46081  dvnmul  46393  dvnprodlem2  46397  fourierdlem83  46639  iundjiun  46910  fcoresf1ob  47537  f1ocof1ob  47545  4an21  47734  sprvalpwn0  47959  pairreueq  47986  prprsprreu  47995  prprreueq  47996  clnbgrel  48320  dfvopnbgr2  48345  rngcinvALTV  48768  ringcinvALTV  48802  mpomptx2  48827  reuxfr1dd  49298  coxp  49324  opnneir  49398  opnneilv  49400  i0oii  49411  io1ii  49412  upfval2  49668