Theorem anass 472

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

Syntax hints:   ↔ wb 209   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  bianass  641  an31  647  an4  655  3anass  1092  3an4anass  1102  an33rean  1480  2sb5  2278  r19.41v  3300  r19.41  3301  rabrab  3332  ceqsex3v  3493  spc2ed  3550  ceqsrex2v  3599  rexrab  3635  rexrab2  3641  2reu5  3697  rexss  3986  inass  4146  rexin  4166  indifdir  4210  difin2  4216  difrab  4229  reupick3  4240  inssdif0  4283  rexdifpr  4558  rexdifsn  4687  reusv2lem4  5267  reusv2  5269  eqvinop  5343  copsexgw  5346  copsexg  5347  rabxp  5564  elvvv  5591  resopab2  5871  difxp  5988  mptpreima  6059  resco  6070  coass  6085  wfi  6149  imadif  6408  dff1o2  6595  eqfnfv3  6781  f1ossf1o  6867  isoini  7070  f1oiso  7083  oprabidw  7166  oprabid  7167  dfoprab2  7191  mpoeq123  7205  mpomptx  7244  resoprab2  7250  ov3  7291  uniuni  7464  elxp4  7609  elxp5  7610  oprabex3  7660  frxp  7803  rexsupp  7831  brtpos2  7881  oeeui  8211  oeeu  8212  omabs  8257  mapsnend  8571  xpsnen  8584  xpcomco  8590  xpassen  8594  wemapsolem  8998  epfrs  9157  aceq1  9528  dfac5lem1  9534  dfac5lem2  9535  dfac5lem5  9538  kmlem3  9563  kmlem14  9574  pwfseqlem1  10069  ltexpi  10313  ltexprlem4  10450  axaddf  10556  axmulf  10557  rexuz  12286  rexuz2  12287  nnwos  12303  zmin  12332  rexrp  12398  elixx3g  12739  elfz2  12892  preduz  13024  fzind2  13150  hashbclem  13806  resqrex  14602  rlim  14844  divalglem10  15743  divalgb  15745  gcdass  15885  lcmass  15948  isprm2  16016  infpn2  16239  ispos2  17550  issubmndb  17962  issubg3  18289  resscntz  18454  subgdmdprd  19149  dprd2d2  19159  dfrhm2  19465  isassa  20545  aspval2  20584  fvmptnn04if  21454  ntreq0  21682  cmpcov2  21995  llyi  22079  nllyi  22080  ptpjpre1  22176  tx1cn  22214  tx2cn  22215  txtube  22245  txkgen  22257  trfil2  22492  elflim2  22569  cnpflfi  22604  isfcls  22614  cnextcn  22672  istlm  22790  blres  23038  metrest  23131  isnlm  23281  elpi1  23650  isclmp  23702  iscvsp  23733  isncvsngp  23754  iscph  23775  cfilucfil3  23924  itg1climres  24318  itgsubst  24652  ulmdvlem3  24997  cubic  25435  vmasum  25800  lgsquadlem1  25964  lgsquadlem2  25965  legov  26379  perpln1  26504  axcontlem5  26762  nbgrel  27130  nbusgredgeu0  27158  nb3grpr2  27173  finsumvtxdg2ssteplem3  27337  usgr2pth0  27554  isclwlke  27566  wwlksnfi  27692  elwwlks2ons3  27741  wpthswwlks2on  27747  usgr2wspthon  27751  rusgrnumwwlkl1  27754  isclwwlk  27769  isclwwlknx  27821  clwlknf1oclwwlkn  27869  clwwlknonel  27880  clwwlknon2x  27888  clwwlkvbij  27898  iseupthf1o  27987  fusgr2wsp2nb  28119  grpoidinvlem3  28289  h2hlm  28763  issh  28991  issh3  29002  ocsh  29066  cvbr2  30066  cvnbtwn2  30070  mdsl2i  30105  cvmdi  30107  mdsymlem2  30187  sumdmdii  30198  dmrab  30267  difrab2  30268  disjunsn  30357  mpomptxf  30442  ressupprn  30450  1stpreima  30466  2ndpreima  30467  f1od2  30483  nndiffz1  30535  omndmul2  30763  smatrcl  31149  crefdf  31201  1stmbfm  31628  2ndmbfm  31629  dya2iocnei  31650  eulerpartlemgvv  31744  eulerpartlemn  31749  bnj250  32081  bnj251  32082  bnj256  32086  bnj168  32110  cusgr3cyclex  32496  iscvm  32619  axacprim  33046  dfpo2  33104  dfdm5  33129  dfrn5  33130  elima4  33132  frpoind  33193  frind  33198  sltval2  33276  madeval2  33403  dfon3  33466  brimg  33511  dfrecs2  33524  dfrdg4  33525  ifscgr  33618  cgrxfr  33629  segcon2  33679  seglecgr12im  33684  segletr  33688  ellines  33726  neifg  33832  bj-dfmpoa  34533  bj-imdiridlem  34600  bj-imdirco  34605  topdifinffinlem  34764  icorempo  34768  difunieq  34791  finxpreclem6  34813  wl-df4-3mintru2  34904  wl-cases2-dnf  34917  curf  35035  uncf  35036  matunitlindflem2  35054  matunitlindf  35055  poimirlem26  35083  poimirlem28  35085  poimirlem30  35087  poimirlem32  35089  poimir  35090  itg2addnc  35111  ftc1anclem5  35134  ftc1anc  35138  areacirclem5  35149  isbnd2  35221  heibor1  35248  anan  35659  inxpxrn  35803  prtlem70  36153  prtlem100  36155  lsateln0  36291  islshpat  36313  lcvbr2  36318  lcvnbtwn2  36323  isopos  36476  cvrval2  36570  cvrnbtwn2  36571  ishlat2  36649  3dim0  36753  islvol5  36875  pmapjat1  37149  pclcmpatN  37197  pclfinclN  37246  cdlemefrs29pre00  37691  cdlemefrs29bpre0  37692  cdlemefrs29cpre1  37694  cdleme32a  37737  cdlemftr3  37861  dvhopellsm  38413  dibelval3  38443  diblsmopel  38467  mapdvalc  38925  mapdval4N  38928  mapdordlem1a  38930  3factsumint2  39310  3factsumint3  39311  3factsumint4  39312  3factsumint  39313  fsuppind  39456  diophrex  39716  rmxdioph  39957  dford4  39970  islmodfg  40013  islssfg2  40015  isdomn3  40148  fgraphopab  40154  k0004lem1  40850  ismnuprim  41002  2sbc5g  41120  limcrecl  42271  dvnmul  42585  dvnprodlem2  42589  fourierdlem83  42831  iundjiun  43099  4an21  43826  sprvalpwn0  44000  pairreueq  44027  prprsprreu  44036  prprreueq  44037  isrnghm  44516  isrnghmmul  44517  rngcinv  44605  rngcinvALTV  44617  ringcinv  44656  ringcinvALTV  44680  mpomptx2  44736