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  2314  r19.41v  3196  r3ex  3205  r19.41  3270  rabrabi  3434  rabrab  3439  ceqsex3v  3506  spc2ed  3559  ceqsrex2v  3615  rexrab  3657  rexrab2  3661  reurab  3662  2reu5  3719  inass  4127  rexin  4150  difin2  4249  difrab  4266  reupick3  4278  inssdif0OLD  4326  rabsneq  4603  rexdifpr  4620  rexdifsn  4757  reusv2lem4  5367  reusv2  5369  eqvinop  5460  eqvinot  5461  copsexgw  5464  copsexgwOLD  5465  copsexg  5466  cotsexgw  5467  rabxp  5703  elvvv  5732  resopab2  6034  difxp  6161  mptpreima  6246  resco  6258  coass  6274  dfpo2  6306  frpoind  6352  imadif  6635  dff1o2  6841  eqfnfv3  7042  f1ossf1o  7140  isoini  7356  f1oiso  7369  riotarab  7429  oprabidw  7461  oprabid  7462  dfoprab2  7488  mpoeq123  7502  mpomptx  7543  resoprab2  7549  ov3  7593  uniuni  7786  elxp4  7944  elxp5  7945  oprabex3  7999  f1od2  8121  frxp  8151  rexsupp  8213  brtpos2  8263  oeeui  8625  oeeu  8626  omabs  8674  eldifsucnn  8687  naddsuc2  8725  curf  8904  uncf  8905  mapsnend  9078  xpsnen  9094  xpcomco  9100  xpassen  9104  wemapsolem  9557  epfrs  9745  frind  9767  aceq1  10209  dfac5lem1  10215  dfac5lem2  10216  dfac5lem5  10219  kmlem3  10244  kmlem14  10255  pwfseqlem1  10756  ltexpi  11000  ltexprlem4  11137  axaddf  11243  axmulf  11244  rexuz  13038  rexuz2  13039  nnwos  13055  zmin  13084  rexrp  13156  elixx3g  13502  elfz2  13659  preduz  13797  fzind2  13936  hashbclem  14610  resqrex  15432  rlim  15677  divalglem10  16587  divalgb  16589  gcdass  16735  lcmass  16804  isprm2  16872  infpn2  17106  ispos2  18504  issubmndb  19015  issubg3  19370  resscntz  19562  subgdmdprd  20265  dprd2d2  20275  omndmul2  20362  dfring3  20533  isrnghm  20686  isrnghmmul  20687  dfrhm2  20719  rngcinv  20904  ringcinv  20938  isdomn3  20981  aspval2  22221  matunitlindflem2  23010  matunitlindf  23011  fvmptnn04if  23182  ntreq0  23410  cmpcov2  23723  llyi  23808  nllyi  23809  ptpjpre1  23905  tx1cn  23943  tx2cn  23944  txtube  23974  txkgen  23986  trfil2  24221  elflim2  24298  cnpflfi  24333  isfcls  24343  cnextcn  24401  istlm  24519  blres  24765  metrest  24858  isnlm  25009  elpi1  25381  isclmp  25433  iscvsp  25464  isncvsngp  25485  iscph  25506  cfilucfil3  25656  itg1climres  26050  itgsubst  26384  ulmdvlem3  26744  cubic  27192  vmasum  27558  lgsquadlem1  27722  lgsquadlem2  27723  ltsval2  28028  madeval2  28234  legov  29063  perpln1  29200  prlngmolem2  29446  axcontlem5  29561  nbgrel  29936  nbusgredgeu0  29964  nb3grpr2  29979  finsumvtxdg2ssteplem3  30143  usgr2pth0  30366  isclwlke  30379  wwlksnfi  30510  elwwlks2ons3  30559  wpthswwlks2on  30568  usgr2wspthon  30572  rusgrnumwwlkl1  30575  isclwwlk  30590  isclwwlknx  30642  clwlknf1oclwwlkn  30690  clwwlknonel  30701  clwwlknon2x  30709  clwwlkvbij  30719  iseupthf1o  30818  fusgr2wsp2nb  30950  grpoidinvlem3  31123  h2hlm  31597  issh  31825  issh3  31836  ocsh  31900  cvbr2  32900  cvnbtwn2  32904  mdsl2i  32939  cvmdi  32941  mdsymlem2  33021  sumdmdii  33032  dmrab  33150  difrab2  33151  disjunsn  33245  mpomptxf  33329  ressupprn  33340  1stpreima  33357  2ndpreima  33358  nndiffz1  33434  1arithufdlem4  34135  r1plmhm  34197  r1pquslmic  34198  extdgfialglem1  34380  smatrcl  34484  crefdf  34536  1stmbfm  34948  2ndmbfm  34949  dya2iocnei  34970  eulerpartlemgvv  35064  eulerpartlemn  35069  bnj250  35388  bnj251  35389  bnj256  35393  bnj168  35417  cusgr3cyclex  36025  iscvm  36148  axacprim  36605  dfdm5  36670  dfrn5  36671  elima4  36673  dfon3  36787  brimg  36832  dfrecs2  36847  dfrdg4  36848  ifscgr  36942  cgrxfr  36953  segcon2  37003  seglecgr12im  37008  segletr  37012  ellines  37050  neifg  37292  bj-axseprep  38135  bj-dfmpoa  38185  bj-imdiridlem  38252  bj-imdirco  38257  topdifinffinlem  38416  icorempo  38420  difunieq  38443  finxpreclem6  38465  wl-df4-3mintru2  38556  wl-cases2-dnf  38590  poimirlem26  38710  poimirlem28  38712  poimirlem30  38714  poimirlem32  38716  poimir  38717  itg2addnc  38738  ftc1anclem5  38761  ftc1anc  38765  areacirclem5  38776  isbnd2  38863  heibor1  38890  anan  39313  br1cnvres  39352  inxpxrn  39496  prtlem70  40060  prtlem100  40062  lsateln0  40198  islshpat  40220  lcvbr2  40225  lcvnbtwn2  40230  isopos  40383  cvrval2  40477  cvrnbtwn2  40478  ishlat2  40556  3dim0  40660  islvol5  40782  pmapjat1  41056  pclcmpatN  41104  pclfinclN  41153  cdlemefrs29pre00  41598  cdlemefrs29bpre0  41599  cdlemefrs29cpre1  41601  cdleme32a  41644  cdlemftr3  41768  dvhopellsm  42320  dibelval3  42350  diblsmopel  42374  mapdvalc  42832  mapdval4N  42835  mapdordlem1a  42837  3factsumint2  43218  3factsumint3  43219  3factsumint4  43220  3factsumint  43221  aks4d1p8  43283  redvmptabs  43557  fimgmcyc  43744  fsuppind  43764  diophrex  43932  rmxdioph  44169  dford4  44182  islmodfg  44217  islssfg2  44219  fgraphopab  44351  cantnftermord  44468  tfsconcatlem  44484  k0004lem1  45293  ismnuprim  45424  2sbc5g  45546  modelaxreplem3  46115  limcrecl  46786  dvnmul  47098  dvnprodlem2  47102  fourierdlem83  47344  iundjiun  47615  fcoresf1ob  48288  f1ocof1ob  48296  4an21  48485  sprvalpwn0  48710  pairreueq  48737  prprsprreu  48746  prprreueq  48747  clnbgrel  49071  dfvopnbgr2  49096  rngcinvALTV  49518  ringcinvALTV  49552  mpomptx2  49592  reuxfr1dd  50062  coxp  50089  opnneir  50166  opnneilv  50168  i0oii  50179  io1ii  50180  upfval2  50438  isnat3  50487  alsanmo  51126  ralsanmo  51127  2alsraln0  51133