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  3167  r3ex  3176  r19.41  3241  rabrabi  3408  rabrab  3413  ceqsex3v  3483  spc2ed  3543  ceqsrex2v  3600  rexrab  3642  rexrab2  3646  reurab  3647  2reu5  3704  rexssOLD  3999  inass  4168  rexin  4190  difin2  4241  difrab  4258  reupick3  4270  inssdif0  4314  rabsneq  4586  rexdifpr  4603  rexdifsn  4739  reusv2lem4  5343  reusv2  5345  eqvinop  5440  copsexgw  5443  copsexgwOLD  5444  copsexg  5445  rabxp  5679  elvvv  5707  resopab2  6001  difxp  6128  mptpreima  6202  resco  6214  coass  6230  dfpo2  6260  frpoind  6306  imadif  6582  dff1o2  6785  eqfnfv3  6985  f1ossf1o  7081  isoini  7293  f1oiso  7306  riotarab  7366  oprabidw  7398  oprabid  7399  dfoprab2  7425  mpoeq123  7439  mpomptx  7480  resoprab2  7486  ov3  7530  uniuni  7716  elxp4  7873  elxp5  7874  oprabex3  7930  frxp  8076  rexsupp  8132  brtpos2  8182  oeeui  8538  oeeu  8539  omabs  8587  eldifsucnn  8600  naddsuc2  8637  mapsnend  8983  xpsnen  8999  xpcomco  9005  xpassen  9009  wemapsolem  9465  epfrs  9652  frind  9674  aceq1  10039  dfac5lem1  10045  dfac5lem2  10046  dfac5lem5  10049  kmlem3  10075  kmlem14  10086  pwfseqlem1  10581  ltexpi  10825  ltexprlem4  10962  axaddf  11068  axmulf  11069  rexuz  12848  rexuz2  12849  nnwos  12865  zmin  12894  rexrp  12965  elixx3g  13311  elfz2  13468  preduz  13604  fzind2  13743  hashbclem  14414  resqrex  15212  rlim  15457  divalglem10  16371  divalgb  16373  gcdass  16516  lcmass  16583  isprm2  16651  infpn2  16884  ispos2  18281  issubmndb  18773  issubg3  19120  resscntz  19308  subgdmdprd  20011  dprd2d2  20021  omndmul2  20108  isrnghm  20421  isrnghmmul  20422  dfrhm2  20454  rngcinv  20614  ringcinv  20648  isdomn3  20692  aspval2  21878  fvmptnn04if  22814  ntreq0  23042  cmpcov2  23355  llyi  23439  nllyi  23440  ptpjpre1  23536  tx1cn  23574  tx2cn  23575  txtube  23605  txkgen  23617  trfil2  23852  elflim2  23929  cnpflfi  23964  isfcls  23974  cnextcn  24032  istlm  24150  blres  24396  metrest  24489  isnlm  24640  elpi1  25012  isclmp  25064  iscvsp  25095  isncvsngp  25116  iscph  25137  cfilucfil3  25287  itg1climres  25681  itgsubst  26016  ulmdvlem3  26367  cubic  26813  vmasum  27179  lgsquadlem1  27343  lgsquadlem2  27344  ltsval2  27620  madeval2  27825  legov  28653  perpln1  28778  axcontlem5  29037  nbgrel  29409  nbusgredgeu0  29437  nb3grpr2  29452  finsumvtxdg2ssteplem3  29616  usgr2pth0  29833  isclwlke  29845  wwlksnfi  29974  elwwlks2ons3  30023  wpthswwlks2on  30032  usgr2wspthon  30036  rusgrnumwwlkl1  30039  isclwwlk  30054  isclwwlknx  30106  clwlknf1oclwwlkn  30154  clwwlknonel  30165  clwwlknon2x  30173  clwwlkvbij  30183  iseupthf1o  30272  fusgr2wsp2nb  30404  grpoidinvlem3  30577  h2hlm  31051  issh  31279  issh3  31290  ocsh  31354  cvbr2  32354  cvnbtwn2  32358  mdsl2i  32393  cvmdi  32395  mdsymlem2  32475  sumdmdii  32486  dmrab  32566  difrab2  32567  disjunsn  32664  mpomptxf  32751  ressupprn  32763  1stpreima  32780  2ndpreima  32781  f1od2  32792  nndiffz1  32859  1arithufdlem4  33607  r1plmhm  33670  r1pquslmic  33671  extdgfialglem1  33836  smatrcl  33940  crefdf  33992  1stmbfm  34404  2ndmbfm  34405  dya2iocnei  34426  eulerpartlemgvv  34520  eulerpartlemn  34525  bnj250  34844  bnj251  34845  bnj256  34849  bnj168  34873  cusgr3cyclex  35318  iscvm  35441  axacprim  35889  dfdm5  35955  dfrn5  35956  elima4  35958  dfon3  36072  brimg  36117  dfrecs2  36132  dfrdg4  36133  ifscgr  36226  cgrxfr  36237  segcon2  36287  seglecgr12im  36292  segletr  36296  ellines  36334  neifg  36553  bj-axseprep  37381  bj-dfmpoa  37430  bj-imdiridlem  37499  bj-imdirco  37504  topdifinffinlem  37663  icorempo  37667  difunieq  37690  finxpreclem6  37712  wl-df4-3mintru2  37803  wl-cases2-dnf  37837  curf  37919  uncf  37920  matunitlindflem2  37938  matunitlindf  37939  poimirlem26  37967  poimirlem28  37969  poimirlem30  37971  poimirlem32  37973  poimir  37974  itg2addnc  37995  ftc1anclem5  38018  ftc1anc  38022  areacirclem5  38033  isbnd2  38104  heibor1  38131  anan  38556  br1cnvres  38595  inxpxrn  38739  prtlem70  39303  prtlem100  39305  lsateln0  39441  islshpat  39463  lcvbr2  39468  lcvnbtwn2  39473  isopos  39626  cvrval2  39720  cvrnbtwn2  39721  ishlat2  39799  3dim0  39903  islvol5  40025  pmapjat1  40299  pclcmpatN  40347  pclfinclN  40396  cdlemefrs29pre00  40841  cdlemefrs29bpre0  40842  cdlemefrs29cpre1  40844  cdleme32a  40887  cdlemftr3  41011  dvhopellsm  41563  dibelval3  41593  diblsmopel  41617  mapdvalc  42075  mapdval4N  42078  mapdordlem1a  42080  3factsumint2  42461  3factsumint3  42462  3factsumint4  42463  3factsumint  42464  aks4d1p8  42526  redvmptabs  42792  fimgmcyc  42979  fsuppind  43023  diophrex  43207  rmxdioph  43444  dford4  43457  islmodfg  43497  islssfg2  43499  fgraphopab  43631  cantnftermord  43748  tfsconcatlem  43764  k0004lem1  44574  ismnuprim  44721  2sbc5g  44843  modelaxreplem3  45407  limcrecl  46059  dvnmul  46371  dvnprodlem2  46375  fourierdlem83  46617  iundjiun  46888  fcoresf1ob  47521  f1ocof1ob  47529  4an21  47718  sprvalpwn0  47943  pairreueq  47970  prprsprreu  47979  prprreueq  47980  clnbgrel  48304  dfvopnbgr2  48329  rngcinvALTV  48752  ringcinvALTV  48786  mpomptx2  48811  reuxfr1dd  49282  coxp  49308  opnneir  49382  opnneilv  49384  i0oii  49395  io1ii  49396  upfval2  49652