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  3420  rabrab  3425  ceqsex3v  3497  spc2ed  3557  ceqsrex2v  3614  rexrab  3656  rexrab2  3660  reurab  3661  2reu5  3718  rexssOLD  4013  inass  4182  rexin  4204  difin2  4255  difrab  4272  reupick3  4284  inssdif0  4328  rabsneq  4601  rexdifpr  4618  rexdifsn  4752  reusv2lem4  5350  reusv2  5352  eqvinop  5445  copsexgw  5448  copsexg  5449  rabxp  5682  elvvv  5710  resopab2  6005  difxp  6132  mptpreima  6206  resco  6218  coass  6234  dfpo2  6264  frpoind  6310  imadif  6586  dff1o2  6789  eqfnfv3  6989  f1ossf1o  7085  isoini  7296  f1oiso  7309  riotarab  7369  oprabidw  7401  oprabid  7402  dfoprab2  7428  mpoeq123  7442  mpomptx  7483  resoprab2  7489  ov3  7533  uniuni  7719  elxp4  7876  elxp5  7877  oprabex3  7933  frxp  8080  rexsupp  8136  brtpos2  8186  oeeui  8542  oeeu  8543  omabs  8591  eldifsucnn  8604  naddsuc2  8641  mapsnend  8987  xpsnen  9003  xpcomco  9009  xpassen  9013  wemapsolem  9469  epfrs  9654  frind  9676  aceq1  10041  dfac5lem1  10047  dfac5lem2  10048  dfac5lem5  10051  kmlem3  10077  kmlem14  10088  pwfseqlem1  10583  ltexpi  10827  ltexprlem4  10964  axaddf  11070  axmulf  11071  rexuz  12825  rexuz2  12826  nnwos  12842  zmin  12871  rexrp  12942  elixx3g  13288  elfz2  13444  preduz  13580  fzind2  13718  hashbclem  14389  resqrex  15187  rlim  15432  divalglem10  16343  divalgb  16345  gcdass  16488  lcmass  16555  isprm2  16623  infpn2  16855  ispos2  18252  issubmndb  18744  issubg3  19091  resscntz  19279  subgdmdprd  19982  dprd2d2  19992  omndmul2  20079  isrnghm  20394  isrnghmmul  20395  dfrhm2  20427  rngcinv  20587  ringcinv  20621  isdomn3  20665  aspval2  21871  fvmptnn04if  22810  ntreq0  23038  cmpcov2  23351  llyi  23435  nllyi  23436  ptpjpre1  23532  tx1cn  23570  tx2cn  23571  txtube  23601  txkgen  23613  trfil2  23848  elflim2  23925  cnpflfi  23960  isfcls  23970  cnextcn  24028  istlm  24146  blres  24392  metrest  24485  isnlm  24636  elpi1  25018  isclmp  25070  iscvsp  25101  isncvsngp  25122  iscph  25143  cfilucfil3  25293  itg1climres  25688  itgsubst  26029  ulmdvlem3  26384  cubic  26832  vmasum  27200  lgsquadlem1  27364  lgsquadlem2  27365  ltsval2  27641  madeval2  27846  legov  28675  perpln1  28800  axcontlem5  29059  nbgrel  29431  nbusgredgeu0  29459  nb3grpr2  29474  finsumvtxdg2ssteplem3  29639  usgr2pth0  29856  isclwlke  29868  wwlksnfi  29997  elwwlks2ons3  30046  wpthswwlks2on  30055  usgr2wspthon  30059  rusgrnumwwlkl1  30062  isclwwlk  30077  isclwwlknx  30129  clwlknf1oclwwlkn  30177  clwwlknonel  30188  clwwlknon2x  30196  clwwlkvbij  30206  iseupthf1o  30295  fusgr2wsp2nb  30427  grpoidinvlem3  30600  h2hlm  31074  issh  31302  issh3  31313  ocsh  31377  cvbr2  32377  cvnbtwn2  32381  mdsl2i  32416  cvmdi  32418  mdsymlem2  32498  sumdmdii  32509  dmrab  32589  difrab2  32590  disjunsn  32687  mpomptxf  32774  ressupprn  32786  1stpreima  32803  2ndpreima  32804  f1od2  32815  nndiffz1  32883  1arithufdlem4  33646  r1plmhm  33709  r1pquslmic  33710  extdgfialglem1  33876  smatrcl  33980  crefdf  34032  1stmbfm  34444  2ndmbfm  34445  dya2iocnei  34466  eulerpartlemgvv  34560  eulerpartlemn  34565  bnj250  34884  bnj251  34885  bnj256  34889  bnj168  34913  cusgr3cyclex  35358  iscvm  35481  axacprim  35929  dfdm5  35995  dfrn5  35996  elima4  35998  dfon3  36112  brimg  36157  dfrecs2  36172  dfrdg4  36173  ifscgr  36266  cgrxfr  36277  segcon2  36327  seglecgr12im  36332  segletr  36336  ellines  36374  neifg  36593  bj-axseprep  37349  bj-dfmpoa  37398  bj-imdiridlem  37467  bj-imdirco  37472  topdifinffinlem  37629  icorempo  37633  difunieq  37656  finxpreclem6  37678  wl-df4-3mintru2  37769  wl-cases2-dnf  37796  curf  37878  uncf  37879  matunitlindflem2  37897  matunitlindf  37898  poimirlem26  37926  poimirlem28  37928  poimirlem30  37930  poimirlem32  37932  poimir  37933  itg2addnc  37954  ftc1anclem5  37977  ftc1anc  37981  areacirclem5  37992  isbnd2  38063  heibor1  38090  anan  38515  br1cnvres  38554  inxpxrn  38698  prtlem70  39262  prtlem100  39264  lsateln0  39400  islshpat  39422  lcvbr2  39427  lcvnbtwn2  39432  isopos  39585  cvrval2  39679  cvrnbtwn2  39680  ishlat2  39758  3dim0  39862  islvol5  39984  pmapjat1  40258  pclcmpatN  40306  pclfinclN  40355  cdlemefrs29pre00  40800  cdlemefrs29bpre0  40801  cdlemefrs29cpre1  40803  cdleme32a  40846  cdlemftr3  40970  dvhopellsm  41522  dibelval3  41552  diblsmopel  41576  mapdvalc  42034  mapdval4N  42037  mapdordlem1a  42039  3factsumint2  42421  3factsumint3  42422  3factsumint4  42423  3factsumint  42424  aks4d1p8  42486  redvmptabs  42759  fimgmcyc  42933  fsuppind  42977  diophrex  43161  rmxdioph  43402  dford4  43415  islmodfg  43455  islssfg2  43457  fgraphopab  43589  cantnftermord  43706  tfsconcatlem  43722  k0004lem1  44532  ismnuprim  44679  2sbc5g  44801  modelaxreplem3  45365  limcrecl  46018  dvnmul  46330  dvnprodlem2  46334  fourierdlem83  46576  iundjiun  46847  fcoresf1ob  47462  f1ocof1ob  47470  4an21  47659  sprvalpwn0  47872  pairreueq  47899  prprsprreu  47908  prprreueq  47909  clnbgrel  48217  dfvopnbgr2  48242  rngcinvALTV  48665  ringcinvALTV  48699  mpomptx2  48724  reuxfr1dd  49195  coxp  49221  opnneir  49295  opnneilv  49297  i0oii  49308  io1ii  49309  upfval2  49565