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  642  an31  648  an4  656  3anass  1094  3an4anass  1104  4anpull2  1362  an33rean  1485  2sb5  2278  r19.41v  3165  r3ex  3174  r19.41  3239  rabrabi  3422  rabrab  3427  ceqsex3v  3500  spc2ed  3564  ceqsrex2v  3621  rexrab  3664  rexrab2  3668  reurab  3669  2reu5  3726  rexssOLD  4021  inass  4187  rexin  4209  difin2  4260  difrab  4277  reupick3  4289  inssdif0  4333  rabsneq  4604  rexdifpr  4619  rexdifsn  4754  reusv2lem4  5351  reusv2  5353  eqvinop  5442  copsexgw  5445  copsexg  5446  rabxp  5679  elvvv  5707  resopab2  5996  difxp  6125  mptpreima  6199  resco  6211  coass  6226  dfpo2  6257  frpoind  6303  imadif  6584  dff1o2  6787  eqfnfv3  6987  f1ossf1o  7082  isoini  7295  f1oiso  7308  riotarab  7368  oprabidw  7400  oprabid  7401  dfoprab2  7427  mpoeq123  7441  mpomptx  7482  resoprab2  7488  ov3  7532  uniuni  7718  elxp4  7878  elxp5  7879  oprabex3  7935  frxp  8082  rexsupp  8138  brtpos2  8188  oeeui  8543  oeeu  8544  omabs  8592  eldifsucnn  8605  naddsuc2  8642  mapsnend  8984  xpsnen  9002  xpcomco  9008  xpassen  9012  wemapsolem  9479  epfrs  9660  frind  9679  aceq1  10046  dfac5lem1  10052  dfac5lem2  10053  dfac5lem5  10056  kmlem3  10082  kmlem14  10093  pwfseqlem1  10587  ltexpi  10831  ltexprlem4  10968  axaddf  11074  axmulf  11075  rexuz  12833  rexuz2  12834  nnwos  12850  zmin  12879  rexrp  12950  elixx3g  13295  elfz2  13451  preduz  13587  fzind2  13722  hashbclem  14393  resqrex  15192  rlim  15437  divalglem10  16348  divalgb  16350  gcdass  16493  lcmass  16560  isprm2  16628  infpn2  16860  ispos2  18256  issubmndb  18714  issubg3  19058  resscntz  19247  subgdmdprd  19950  dprd2d2  19960  omndmul2  20047  isrnghm  20361  isrnghmmul  20362  dfrhm2  20394  rngcinv  20557  ringcinv  20591  isdomn3  20635  aspval2  21840  fvmptnn04if  22769  ntreq0  22997  cmpcov2  23310  llyi  23394  nllyi  23395  ptpjpre1  23491  tx1cn  23529  tx2cn  23530  txtube  23560  txkgen  23572  trfil2  23807  elflim2  23884  cnpflfi  23919  isfcls  23929  cnextcn  23987  istlm  24105  blres  24352  metrest  24445  isnlm  24596  elpi1  24978  isclmp  25030  iscvsp  25061  isncvsngp  25082  iscph  25103  cfilucfil3  25253  itg1climres  25648  itgsubst  25989  ulmdvlem3  26344  cubic  26792  vmasum  27160  lgsquadlem1  27324  lgsquadlem2  27325  sltval2  27601  madeval2  27798  legov  28565  perpln1  28690  axcontlem5  28948  nbgrel  29320  nbusgredgeu0  29348  nb3grpr2  29363  finsumvtxdg2ssteplem3  29528  usgr2pth0  29745  isclwlke  29757  wwlksnfi  29886  elwwlks2ons3  29935  wpthswwlks2on  29941  usgr2wspthon  29945  rusgrnumwwlkl1  29948  isclwwlk  29963  isclwwlknx  30015  clwlknf1oclwwlkn  30063  clwwlknonel  30074  clwwlknon2x  30082  clwwlkvbij  30092  iseupthf1o  30181  fusgr2wsp2nb  30313  grpoidinvlem3  30485  h2hlm  30959  issh  31187  issh3  31198  ocsh  31262  cvbr2  32262  cvnbtwn2  32266  mdsl2i  32301  cvmdi  32303  mdsymlem2  32383  sumdmdii  32394  dmrab  32476  difrab2  32477  disjunsn  32573  mpomptxf  32651  ressupprn  32663  1stpreima  32680  2ndpreima  32681  f1od2  32694  nndiffz1  32759  1arithufdlem4  33511  r1plmhm  33568  r1pquslmic  33569  smatrcl  33779  crefdf  33831  1stmbfm  34244  2ndmbfm  34245  dya2iocnei  34266  eulerpartlemgvv  34360  eulerpartlemn  34365  bnj250  34684  bnj251  34685  bnj256  34689  bnj168  34713  cusgr3cyclex  35116  iscvm  35239  axacprim  35687  dfdm5  35753  dfrn5  35754  elima4  35756  dfon3  35873  brimg  35918  dfrecs2  35931  dfrdg4  35932  ifscgr  36025  cgrxfr  36036  segcon2  36086  seglecgr12im  36091  segletr  36095  ellines  36133  neifg  36352  bj-dfmpoa  37099  bj-imdiridlem  37166  bj-imdirco  37171  topdifinffinlem  37328  icorempo  37332  difunieq  37355  finxpreclem6  37377  wl-df4-3mintru2  37468  wl-cases2-dnf  37493  curf  37585  uncf  37586  matunitlindflem2  37604  matunitlindf  37605  poimirlem26  37633  poimirlem28  37635  poimirlem30  37637  poimirlem32  37639  poimir  37640  itg2addnc  37661  ftc1anclem5  37684  ftc1anc  37688  areacirclem5  37699  isbnd2  37770  heibor1  37797  anan  38210  br1cnvres  38251  inxpxrn  38374  prtlem70  38843  prtlem100  38845  lsateln0  38981  islshpat  39003  lcvbr2  39008  lcvnbtwn2  39013  isopos  39166  cvrval2  39260  cvrnbtwn2  39261  ishlat2  39339  3dim0  39444  islvol5  39566  pmapjat1  39840  pclcmpatN  39888  pclfinclN  39937  cdlemefrs29pre00  40382  cdlemefrs29bpre0  40383  cdlemefrs29cpre1  40385  cdleme32a  40428  cdlemftr3  40552  dvhopellsm  41104  dibelval3  41134  diblsmopel  41158  mapdvalc  41616  mapdval4N  41619  mapdordlem1a  41621  3factsumint2  42003  3factsumint3  42004  3factsumint4  42005  3factsumint  42006  aks4d1p8  42068  redvmptabs  42341  fimgmcyc  42515  fsuppind  42571  diophrex  42756  rmxdioph  42998  dford4  43011  islmodfg  43051  islssfg2  43053  fgraphopab  43185  cantnftermord  43302  tfsconcatlem  43318  k0004lem1  44129  ismnuprim  44276  2sbc5g  44398  modelaxreplem3  44963  limcrecl  45620  dvnmul  45934  dvnprodlem2  45938  fourierdlem83  46180  iundjiun  46451  fcoresf1ob  47067  f1ocof1ob  47075  4an21  47264  sprvalpwn0  47477  pairreueq  47504  prprsprreu  47513  prprreueq  47514  clnbgrel  47822  dfvopnbgr2  47846  rngcinvALTV  48257  ringcinvALTV  48291  mpomptx2  48316  reuxfr1dd  48788  coxp  48814  opnneir  48888  opnneilv  48890  i0oii  48901  io1ii  48902  upfval2  49159