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  3159  r3ex  3168  r19.41  3233  rabrabi  3414  rabrab  3419  ceqsex3v  3492  spc2ed  3556  ceqsrex2v  3613  rexrab  3656  rexrab2  3660  reurab  3661  2reu5  3718  rexssOLD  4013  inass  4179  rexin  4201  difin2  4252  difrab  4269  reupick3  4281  inssdif0  4325  rabsneq  4596  rexdifpr  4611  rexdifsn  4745  reusv2lem4  5340  reusv2  5342  eqvinop  5430  copsexgw  5433  copsexg  5434  rabxp  5667  elvvv  5695  resopab2  5987  difxp  6113  mptpreima  6187  resco  6199  coass  6214  dfpo2  6244  frpoind  6290  imadif  6566  dff1o2  6769  eqfnfv3  6967  f1ossf1o  7062  isoini  7275  f1oiso  7288  riotarab  7348  oprabidw  7380  oprabid  7381  dfoprab2  7407  mpoeq123  7421  mpomptx  7462  resoprab2  7468  ov3  7512  uniuni  7698  elxp4  7855  elxp5  7856  oprabex3  7912  frxp  8059  rexsupp  8115  brtpos2  8165  oeeui  8520  oeeu  8521  omabs  8569  eldifsucnn  8582  naddsuc2  8619  mapsnend  8961  xpsnen  8978  xpcomco  8984  xpassen  8988  wemapsolem  9442  epfrs  9627  frind  9646  aceq1  10011  dfac5lem1  10017  dfac5lem2  10018  dfac5lem5  10021  kmlem3  10047  kmlem14  10058  pwfseqlem1  10552  ltexpi  10796  ltexprlem4  10933  axaddf  11039  axmulf  11040  rexuz  12799  rexuz2  12800  nnwos  12816  zmin  12845  rexrp  12916  elixx3g  13261  elfz2  13417  preduz  13553  fzind2  13688  hashbclem  14359  resqrex  15157  rlim  15402  divalglem10  16313  divalgb  16315  gcdass  16458  lcmass  16525  isprm2  16593  infpn2  16825  ispos2  18221  issubmndb  18679  issubg3  19023  resscntz  19212  subgdmdprd  19915  dprd2d2  19925  omndmul2  20012  isrnghm  20326  isrnghmmul  20327  dfrhm2  20359  rngcinv  20522  ringcinv  20556  isdomn3  20600  aspval2  21805  fvmptnn04if  22734  ntreq0  22962  cmpcov2  23275  llyi  23359  nllyi  23360  ptpjpre1  23456  tx1cn  23494  tx2cn  23495  txtube  23525  txkgen  23537  trfil2  23772  elflim2  23849  cnpflfi  23884  isfcls  23894  cnextcn  23952  istlm  24070  blres  24317  metrest  24410  isnlm  24561  elpi1  24943  isclmp  24995  iscvsp  25026  isncvsngp  25047  iscph  25068  cfilucfil3  25218  itg1climres  25613  itgsubst  25954  ulmdvlem3  26309  cubic  26757  vmasum  27125  lgsquadlem1  27289  lgsquadlem2  27290  sltval2  27566  madeval2  27763  legov  28530  perpln1  28655  axcontlem5  28913  nbgrel  29285  nbusgredgeu0  29313  nb3grpr2  29328  finsumvtxdg2ssteplem3  29493  usgr2pth0  29710  isclwlke  29722  wwlksnfi  29851  elwwlks2ons3  29900  wpthswwlks2on  29906  usgr2wspthon  29910  rusgrnumwwlkl1  29913  isclwwlk  29928  isclwwlknx  29980  clwlknf1oclwwlkn  30028  clwwlknonel  30039  clwwlknon2x  30047  clwwlkvbij  30057  iseupthf1o  30146  fusgr2wsp2nb  30278  grpoidinvlem3  30450  h2hlm  30924  issh  31152  issh3  31163  ocsh  31227  cvbr2  32227  cvnbtwn2  32231  mdsl2i  32266  cvmdi  32268  mdsymlem2  32348  sumdmdii  32359  dmrab  32441  difrab2  32442  disjunsn  32538  mpomptxf  32621  ressupprn  32633  1stpreima  32650  2ndpreima  32651  f1od2  32664  nndiffz1  32730  1arithufdlem4  33485  r1plmhm  33543  r1pquslmic  33544  extdgfialglem1  33665  smatrcl  33769  crefdf  33821  1stmbfm  34234  2ndmbfm  34235  dya2iocnei  34256  eulerpartlemgvv  34350  eulerpartlemn  34355  bnj250  34674  bnj251  34675  bnj256  34679  bnj168  34703  cusgr3cyclex  35119  iscvm  35242  axacprim  35690  dfdm5  35756  dfrn5  35757  elima4  35759  dfon3  35876  brimg  35921  dfrecs2  35934  dfrdg4  35935  ifscgr  36028  cgrxfr  36039  segcon2  36089  seglecgr12im  36094  segletr  36098  ellines  36136  neifg  36355  bj-dfmpoa  37102  bj-imdiridlem  37169  bj-imdirco  37174  topdifinffinlem  37331  icorempo  37335  difunieq  37358  finxpreclem6  37380  wl-df4-3mintru2  37471  wl-cases2-dnf  37496  curf  37588  uncf  37589  matunitlindflem2  37607  matunitlindf  37608  poimirlem26  37636  poimirlem28  37638  poimirlem30  37640  poimirlem32  37642  poimir  37643  itg2addnc  37664  ftc1anclem5  37687  ftc1anc  37691  areacirclem5  37702  isbnd2  37773  heibor1  37800  anan  38213  br1cnvres  38254  inxpxrn  38377  prtlem70  38846  prtlem100  38848  lsateln0  38984  islshpat  39006  lcvbr2  39011  lcvnbtwn2  39016  isopos  39169  cvrval2  39263  cvrnbtwn2  39264  ishlat2  39342  3dim0  39446  islvol5  39568  pmapjat1  39842  pclcmpatN  39890  pclfinclN  39939  cdlemefrs29pre00  40384  cdlemefrs29bpre0  40385  cdlemefrs29cpre1  40387  cdleme32a  40430  cdlemftr3  40554  dvhopellsm  41106  dibelval3  41136  diblsmopel  41160  mapdvalc  41618  mapdval4N  41621  mapdordlem1a  41623  3factsumint2  42005  3factsumint3  42006  3factsumint4  42007  3factsumint  42008  aks4d1p8  42070  redvmptabs  42343  fimgmcyc  42517  fsuppind  42573  diophrex  42758  rmxdioph  42999  dford4  43012  islmodfg  43052  islssfg2  43054  fgraphopab  43186  cantnftermord  43303  tfsconcatlem  43319  k0004lem1  44130  ismnuprim  44277  2sbc5g  44399  modelaxreplem3  44964  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  47847  rngcinvALTV  48270  ringcinvALTV  48304  mpomptx2  48329  reuxfr1dd  48801  coxp  48827  opnneir  48901  opnneilv  48903  i0oii  48914  io1ii  48915  upfval2  49172