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  3167  r3ex  3176  r19.41  3241  rabrabi  3425  rabrab  3430  ceqsex3v  3503  spc2ed  3567  ceqsrex2v  3624  rexrab  3667  rexrab2  3671  reurab  3672  2reu5  3729  rexssOLD  4024  inass  4191  rexin  4213  difin2  4264  difrab  4281  reupick3  4293  inssdif0  4337  rabsneq  4608  rexdifpr  4623  rexdifsn  4758  reusv2lem4  5356  reusv2  5358  eqvinop  5447  copsexgw  5450  copsexg  5451  rabxp  5686  elvvv  5714  resopab2  6007  difxp  6137  mptpreima  6211  resco  6223  coass  6238  dfpo2  6269  frpoind  6315  imadif  6600  dff1o2  6805  eqfnfv3  7005  f1ossf1o  7100  isoini  7313  f1oiso  7326  riotarab  7386  oprabidw  7418  oprabid  7419  dfoprab2  7447  mpoeq123  7461  mpomptx  7502  resoprab2  7508  ov3  7552  uniuni  7738  elxp4  7898  elxp5  7899  oprabex3  7956  frxp  8105  rexsupp  8161  brtpos2  8211  oeeui  8566  oeeu  8567  omabs  8615  eldifsucnn  8628  naddsuc2  8665  mapsnend  9007  xpsnen  9025  xpcomco  9031  xpassen  9035  wemapsolem  9503  epfrs  9684  frind  9703  aceq1  10070  dfac5lem1  10076  dfac5lem2  10077  dfac5lem5  10080  kmlem3  10106  kmlem14  10117  pwfseqlem1  10611  ltexpi  10855  ltexprlem4  10992  axaddf  11098  axmulf  11099  rexuz  12857  rexuz2  12858  nnwos  12874  zmin  12903  rexrp  12974  elixx3g  13319  elfz2  13475  preduz  13611  fzind2  13746  hashbclem  14417  resqrex  15216  rlim  15461  divalglem10  16372  divalgb  16374  gcdass  16517  lcmass  16584  isprm2  16652  infpn2  16884  ispos2  18276  issubmndb  18732  issubg3  19076  resscntz  19265  subgdmdprd  19966  dprd2d2  19976  isrnghm  20350  isrnghmmul  20351  dfrhm2  20383  rngcinv  20546  ringcinv  20580  isdomn3  20624  aspval2  21807  fvmptnn04if  22736  ntreq0  22964  cmpcov2  23277  llyi  23361  nllyi  23362  ptpjpre1  23458  tx1cn  23496  tx2cn  23497  txtube  23527  txkgen  23539  trfil2  23774  elflim2  23851  cnpflfi  23886  isfcls  23896  cnextcn  23954  istlm  24072  blres  24319  metrest  24412  isnlm  24563  elpi1  24945  isclmp  24997  iscvsp  25028  isncvsngp  25049  iscph  25070  cfilucfil3  25220  itg1climres  25615  itgsubst  25956  ulmdvlem3  26311  cubic  26759  vmasum  27127  lgsquadlem1  27291  lgsquadlem2  27292  sltval2  27568  madeval2  27761  legov  28512  perpln1  28637  axcontlem5  28895  nbgrel  29267  nbusgredgeu0  29295  nb3grpr2  29310  finsumvtxdg2ssteplem3  29475  usgr2pth0  29695  isclwlke  29707  wwlksnfi  29836  elwwlks2ons3  29885  wpthswwlks2on  29891  usgr2wspthon  29895  rusgrnumwwlkl1  29898  isclwwlk  29913  isclwwlknx  29965  clwlknf1oclwwlkn  30013  clwwlknonel  30024  clwwlknon2x  30032  clwwlkvbij  30042  iseupthf1o  30131  fusgr2wsp2nb  30263  grpoidinvlem3  30435  h2hlm  30909  issh  31137  issh3  31148  ocsh  31212  cvbr2  32212  cvnbtwn2  32216  mdsl2i  32251  cvmdi  32253  mdsymlem2  32333  sumdmdii  32344  dmrab  32426  difrab2  32427  disjunsn  32523  mpomptxf  32601  ressupprn  32613  1stpreima  32630  2ndpreima  32631  f1od2  32644  nndiffz1  32709  omndmul2  33026  1arithufdlem4  33518  r1plmhm  33575  r1pquslmic  33576  smatrcl  33786  crefdf  33838  1stmbfm  34251  2ndmbfm  34252  dya2iocnei  34273  eulerpartlemgvv  34367  eulerpartlemn  34372  bnj250  34691  bnj251  34692  bnj256  34696  bnj168  34720  cusgr3cyclex  35123  iscvm  35246  axacprim  35694  dfdm5  35760  dfrn5  35761  elima4  35763  dfon3  35880  brimg  35925  dfrecs2  35938  dfrdg4  35939  ifscgr  36032  cgrxfr  36043  segcon2  36093  seglecgr12im  36098  segletr  36102  ellines  36140  neifg  36359  bj-dfmpoa  37106  bj-imdiridlem  37173  bj-imdirco  37178  topdifinffinlem  37335  icorempo  37339  difunieq  37362  finxpreclem6  37384  wl-df4-3mintru2  37475  wl-cases2-dnf  37500  curf  37592  uncf  37593  matunitlindflem2  37611  matunitlindf  37612  poimirlem26  37640  poimirlem28  37642  poimirlem30  37644  poimirlem32  37646  poimir  37647  itg2addnc  37668  ftc1anclem5  37691  ftc1anc  37695  areacirclem5  37706  isbnd2  37777  heibor1  37804  anan  38217  br1cnvres  38258  inxpxrn  38381  prtlem70  38850  prtlem100  38852  lsateln0  38988  islshpat  39010  lcvbr2  39015  lcvnbtwn2  39020  isopos  39173  cvrval2  39267  cvrnbtwn2  39268  ishlat2  39346  3dim0  39451  islvol5  39573  pmapjat1  39847  pclcmpatN  39895  pclfinclN  39944  cdlemefrs29pre00  40389  cdlemefrs29bpre0  40390  cdlemefrs29cpre1  40392  cdleme32a  40435  cdlemftr3  40559  dvhopellsm  41111  dibelval3  41141  diblsmopel  41165  mapdvalc  41623  mapdval4N  41626  mapdordlem1a  41628  3factsumint2  42010  3factsumint3  42011  3factsumint4  42012  3factsumint  42013  aks4d1p8  42075  redvmptabs  42348  fimgmcyc  42522  fsuppind  42578  diophrex  42763  rmxdioph  43005  dford4  43018  islmodfg  43058  islssfg2  43060  fgraphopab  43192  cantnftermord  43309  tfsconcatlem  43325  k0004lem1  44136  ismnuprim  44283  2sbc5g  44405  modelaxreplem3  44970  limcrecl  45627  dvnmul  45941  dvnprodlem2  45945  fourierdlem83  46187  iundjiun  46458  fcoresf1ob  47074  f1ocof1ob  47082  4an21  47271  sprvalpwn0  47484  pairreueq  47511  prprsprreu  47520  prprreueq  47521  clnbgrel  47829  dfvopnbgr2  47853  rngcinvALTV  48264  ringcinvALTV  48298  mpomptx2  48323  reuxfr1dd  48795  coxp  48821  opnneir  48895  opnneilv  48897  i0oii  48908  io1ii  48909  upfval2  49166