Theorem anass 473

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

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

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 401

This theorem is used by:  bianass  654  an31  660  an4  668  3anass  1111  3an4anass  1122  4anpull2OLD  1383  an33rean  1514  2sb5  2313  r19.41v  3195  r3ex  3204  r19.41  3269  rabrabi  3435  rabrab  3440  ceqsex3v  3507  spc2ed  3560  ceqsrex2v  3617  rexrab  3659  rexrab2  3663  reurab  3664  2reu5  3721  rexssOLD  4013  inass  4180  rexin  4203  difin2  4254  difrab  4271  reupick3  4283  inssdif0OLD  4330  rabsneq  4608  rexdifpr  4625  rexdifsn  4762  reusv2lem4  5372  reusv2  5374  eqvinop  5469  copsexgw  5472  copsexgwOLD  5473  copsexg  5474  rabxp  5709  elvvv  5737  resopab2  6038  difxp  6161  mptpreima  6239  resco  6251  coass  6267  dfpo2  6297  frpoind  6343  imadif  6620  dff1o2  6826  eqfnfv3  7027  f1ossf1o  7124  isoini  7336  f1oiso  7349  riotarab  7409  oprabidw  7441  oprabid  7442  dfoprab2  7468  mpoeq123  7482  mpomptx  7523  resoprab2  7529  ov3  7573  uniuni  7757  elxp4  7915  elxp5  7916  oprabex3  7970  frxp  8118  rexsupp  8174  brtpos2  8224  oeeui  8584  oeeu  8585  omabs  8633  eldifsucnn  8646  naddsuc2  8684  mapsnend  9029  xpsnen  9045  xpcomco  9051  xpassen  9055  wemapsolem  9508  epfrs  9696  frind  9718  aceq1  10106  dfac5lem1  10112  dfac5lem2  10113  dfac5lem5  10116  kmlem3  10141  kmlem14  10152  pwfseqlem1  10647  ltexpi  10891  ltexprlem4  11028  axaddf  11134  axmulf  11135  rexuz  12926  rexuz2  12927  nnwos  12943  zmin  12972  rexrp  13043  elixx3g  13389  elfz2  13546  preduz  13683  fzind2  13822  hashbclem  14494  resqrex  15306  rlim  15551  divalglem10  16464  divalgb  16466  gcdass  16609  lcmass  16676  isprm2  16744  infpn2  16977  ispos2  18375  issubmndb  18867  issubg3  19215  resscntz  19407  subgdmdprd  20110  dprd2d2  20120  omndmul2  20207  isrnghm  20528  isrnghmmul  20529  dfrhm2  20561  rngcinv  20745  ringcinv  20779  isdomn3  20822  aspval2  22057  fvmptnn04if  23015  ntreq0  23243  cmpcov2  23556  llyi  23640  nllyi  23641  ptpjpre1  23737  tx1cn  23775  tx2cn  23776  txtube  23806  txkgen  23818  trfil2  24053  elflim2  24130  cnpflfi  24165  isfcls  24175  cnextcn  24233  istlm  24351  blres  24597  metrest  24690  isnlm  24841  elpi1  25213  isclmp  25265  iscvsp  25296  isncvsngp  25317  iscph  25338  cfilucfil3  25488  itg1climres  25882  itgsubst  26217  ulmdvlem3  26574  cubic  27023  vmasum  27389  lgsquadlem1  27553  lgsquadlem2  27554  ltsval2  27829  madeval2  28035  legov  28863  perpln1  28999  prlngmolem2  29212  axcontlem5  29327  nbgrel  29699  nbusgredgeu0  29727  nb3grpr2  29742  finsumvtxdg2ssteplem3  29906  usgr2pth0  30123  isclwlke  30135  wwlksnfi  30264  elwwlks2ons3  30313  wpthswwlks2on  30322  usgr2wspthon  30326  rusgrnumwwlkl1  30329  isclwwlk  30344  isclwwlknx  30396  clwlknf1oclwwlkn  30444  clwwlknonel  30455  clwwlknon2x  30463  clwwlkvbij  30473  iseupthf1o  30562  fusgr2wsp2nb  30694  grpoidinvlem3  30867  h2hlm  31341  issh  31569  issh3  31580  ocsh  31644  cvbr2  32644  cvnbtwn2  32648  mdsl2i  32683  cvmdi  32685  mdsymlem2  32765  sumdmdii  32776  dmrab  32852  difrab2  32853  disjunsn  32948  mpomptxf  33032  ressupprn  33044  1stpreima  33061  2ndpreima  33062  f1od2  33073  nndiffz1  33140  1arithufdlem4  33846  r1plmhm  33908  r1pquslmic  33909  extdgfialglem1  34091  smatrcl  34195  crefdf  34247  1stmbfm  34659  2ndmbfm  34660  dya2iocnei  34681  eulerpartlemgvv  34775  eulerpartlemn  34780  bnj250  35099  bnj251  35100  bnj256  35104  bnj168  35128  cusgr3cyclex  35636  iscvm  35759  axacprim  36207  dfdm5  36273  dfrn5  36274  elima4  36276  dfon3  36390  brimg  36435  dfrecs2  36450  dfrdg4  36451  ifscgr  36544  cgrxfr  36555  segcon2  36605  seglecgr12im  36610  segletr  36614  ellines  36652  neifg  36910  bj-axseprep  37739  bj-dfmpoa  37788  bj-imdiridlem  37857  bj-imdirco  37862  topdifinffinlem  38021  icorempo  38025  difunieq  38048  finxpreclem6  38070  wl-df4-3mintru2  38161  wl-cases2-dnf  38195  curf  38277  uncf  38278  matunitlindflem2  38296  matunitlindf  38297  poimirlem26  38325  poimirlem28  38327  poimirlem30  38329  poimirlem32  38331  poimir  38332  itg2addnc  38353  ftc1anclem5  38376  ftc1anc  38380  areacirclem5  38391  isbnd2  38462  heibor1  38489  anan  38912  br1cnvres  38951  inxpxrn  39095  prtlem70  39659  prtlem100  39661  lsateln0  39797  islshpat  39819  lcvbr2  39824  lcvnbtwn2  39829  isopos  39982  cvrval2  40076  cvrnbtwn2  40077  ishlat2  40155  3dim0  40259  islvol5  40381  pmapjat1  40655  pclcmpatN  40703  pclfinclN  40752  cdlemefrs29pre00  41197  cdlemefrs29bpre0  41198  cdlemefrs29cpre1  41200  cdleme32a  41243  cdlemftr3  41367  dvhopellsm  41919  dibelval3  41949  diblsmopel  41973  mapdvalc  42431  mapdval4N  42434  mapdordlem1a  42436  3factsumint2  42817  3factsumint3  42818  3factsumint4  42819  3factsumint  42820  aks4d1p8  42882  redvmptabs  43149  fimgmcyc  43330  fsuppind  43350  diophrex  43534  rmxdioph  43771  dford4  43784  islmodfg  43824  islssfg2  43826  fgraphopab  43958  cantnftermord  44075  tfsconcatlem  44091  k0004lem1  44901  ismnuprim  45032  2sbc5g  45154  modelaxreplem3  45717  limcrecl  46373  dvnmul  46685  dvnprodlem2  46689  fourierdlem83  46931  iundjiun  47202  fcoresf1ob  47838  f1ocof1ob  47846  4an21  48035  sprvalpwn0  48260  pairreueq  48287  prprsprreu  48296  prprreueq  48297  clnbgrel  48621  dfvopnbgr2  48646  rngcinvALTV  49069  ringcinvALTV  49103  mpomptx2  49143  reuxfr1dd  49613  coxp  49639  opnneir  49713  opnneilv  49715  i0oii  49726  io1ii  49727  upfval2  49983  alsanmo  50616  ralsanmo  50617  2alsraln0  50623