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  2315  r19.41v  3197  r3ex  3206  r19.41  3271  rabrabi  3437  rabrab  3442  ceqsex3v  3509  spc2ed  3562  ceqsrex2v  3619  rexrab  3661  rexrab2  3665  reurab  3666  2reu5  3723  rexssOLD  4014  inass  4180  rexin  4203  difin2  4254  difrab  4271  reupick3  4283  inssdif0OLD  4330  rabsneq  4610  rexdifpr  4627  rexdifsn  4764  reusv2lem4  5374  reusv2  5376  eqvinop  5471  copsexgw  5474  copsexgwOLD  5475  copsexg  5476  rabxp  5711  elvvv  5739  resopab2  6040  difxp  6164  mptpreima  6242  resco  6254  coass  6270  dfpo2  6302  frpoind  6348  imadif  6625  dff1o2  6831  eqfnfv3  7032  f1ossf1o  7129  isoini  7346  f1oiso  7359  riotarab  7419  oprabidw  7451  oprabid  7452  dfoprab2  7478  mpoeq123  7492  mpomptx  7533  resoprab2  7539  ov3  7583  uniuni  7768  elxp4  7926  elxp5  7927  oprabex3  7981  frxp  8129  rexsupp  8185  brtpos2  8235  oeeui  8595  oeeu  8596  omabs  8644  eldifsucnn  8657  naddsuc2  8695  mapsnend  9041  xpsnen  9057  xpcomco  9063  xpassen  9067  wemapsolem  9520  epfrs  9708  frind  9730  aceq1  10118  dfac5lem1  10124  dfac5lem2  10125  dfac5lem5  10128  kmlem3  10153  kmlem14  10164  pwfseqlem1  10663  ltexpi  10907  ltexprlem4  11044  axaddf  11150  axmulf  11151  rexuz  12943  rexuz2  12944  nnwos  12960  zmin  12989  rexrp  13060  elixx3g  13406  elfz2  13563  preduz  13700  fzind2  13839  hashbclem  14512  resqrex  15330  rlim  15575  divalglem10  16487  divalgb  16489  gcdass  16632  lcmass  16699  isprm2  16767  infpn2  17000  ispos2  18398  issubmndb  18905  issubg3  19260  resscntz  19452  subgdmdprd  20155  dprd2d2  20165  omndmul2  20252  isrnghm  20574  isrnghmmul  20575  dfrhm2  20607  rngcinv  20791  ringcinv  20825  isdomn3  20868  aspval2  22103  fvmptnn04if  23061  ntreq0  23289  cmpcov2  23602  llyi  23687  nllyi  23688  ptpjpre1  23784  tx1cn  23822  tx2cn  23823  txtube  23853  txkgen  23865  trfil2  24100  elflim2  24177  cnpflfi  24212  isfcls  24222  cnextcn  24280  istlm  24398  blres  24644  metrest  24737  isnlm  24888  elpi1  25260  isclmp  25312  iscvsp  25343  isncvsngp  25364  iscph  25385  cfilucfil3  25535  itg1climres  25929  itgsubst  26264  ulmdvlem3  26621  cubic  27070  vmasum  27436  lgsquadlem1  27600  lgsquadlem2  27601  ltsval2  27876  madeval2  28082  legov  28910  perpln1  29046  prlngmolem2  29263  axcontlem5  29378  nbgrel  29753  nbusgredgeu0  29781  nb3grpr2  29796  finsumvtxdg2ssteplem3  29960  usgr2pth0  30183  isclwlke  30196  wwlksnfi  30327  elwwlks2ons3  30376  wpthswwlks2on  30385  usgr2wspthon  30389  rusgrnumwwlkl1  30392  isclwwlk  30407  isclwwlknx  30459  clwlknf1oclwwlkn  30507  clwwlknonel  30518  clwwlknon2x  30526  clwwlkvbij  30536  iseupthf1o  30629  fusgr2wsp2nb  30761  grpoidinvlem3  30934  h2hlm  31408  issh  31636  issh3  31647  ocsh  31711  cvbr2  32711  cvnbtwn2  32715  mdsl2i  32750  cvmdi  32752  mdsymlem2  32832  sumdmdii  32843  dmrab  32919  difrab2  32920  disjunsn  33015  mpomptxf  33099  ressupprn  33111  1stpreima  33128  2ndpreima  33129  f1od2  33139  nndiffz1  33206  1arithufdlem4  33906  r1plmhm  33968  r1pquslmic  33969  extdgfialglem1  34151  smatrcl  34255  crefdf  34307  1stmbfm  34720  2ndmbfm  34721  dya2iocnei  34742  eulerpartlemgvv  34836  eulerpartlemn  34841  bnj250  35160  bnj251  35161  bnj256  35165  bnj168  35189  cusgr3cyclex  35674  iscvm  35793  axacprim  36241  dfdm5  36307  dfrn5  36308  elima4  36310  dfon3  36424  brimg  36469  dfrecs2  36484  dfrdg4  36485  ifscgr  36578  cgrxfr  36589  segcon2  36639  seglecgr12im  36644  segletr  36648  ellines  36686  neifg  36944  bj-axseprep  37773  bj-dfmpoa  37822  bj-imdiridlem  37891  bj-imdirco  37896  topdifinffinlem  38055  icorempo  38059  difunieq  38082  finxpreclem6  38104  wl-df4-3mintru2  38195  wl-cases2-dnf  38229  curf  38311  uncf  38312  matunitlindflem2  38330  matunitlindf  38331  poimirlem26  38359  poimirlem28  38361  poimirlem30  38363  poimirlem32  38365  poimir  38366  itg2addnc  38387  ftc1anclem5  38410  ftc1anc  38414  areacirclem5  38425  isbnd2  38497  heibor1  38524  anan  38947  br1cnvres  38986  inxpxrn  39130  prtlem70  39694  prtlem100  39696  lsateln0  39832  islshpat  39854  lcvbr2  39859  lcvnbtwn2  39864  isopos  40017  cvrval2  40111  cvrnbtwn2  40112  ishlat2  40190  3dim0  40294  islvol5  40416  pmapjat1  40690  pclcmpatN  40738  pclfinclN  40787  cdlemefrs29pre00  41232  cdlemefrs29bpre0  41233  cdlemefrs29cpre1  41235  cdleme32a  41278  cdlemftr3  41402  dvhopellsm  41954  dibelval3  41984  diblsmopel  42008  mapdvalc  42466  mapdval4N  42469  mapdordlem1a  42471  3factsumint2  42852  3factsumint3  42853  3factsumint4  42854  3factsumint  42855  aks4d1p8  42917  redvmptabs  43199  fimgmcyc  43380  fsuppind  43400  diophrex  43584  rmxdioph  43821  dford4  43834  islmodfg  43874  islssfg2  43876  fgraphopab  44008  cantnftermord  44125  tfsconcatlem  44141  k0004lem1  44951  ismnuprim  45082  2sbc5g  45204  modelaxreplem3  45767  limcrecl  46423  dvnmul  46735  dvnprodlem2  46739  fourierdlem83  46981  iundjiun  47252  fcoresf1ob  47888  f1ocof1ob  47896  4an21  48085  sprvalpwn0  48310  pairreueq  48337  prprsprreu  48346  prprreueq  48347  clnbgrel  48671  dfvopnbgr2  48696  rngcinvALTV  49118  ringcinvALTV  49152  mpomptx2  49192  reuxfr1dd  49662  coxp  49688  opnneir  49762  opnneilv  49764  i0oii  49775  io1ii  49776  upfval2  50032  alsanmo  50665  ralsanmo  50666  2alsraln0  50672