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 208	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 205   ∧ 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 206  df-an 396

This theorem is referenced by:  bianass  638  an31  644  an4  652  3anass  1093  3an4anass  1103  an33rean  1481  2sb5  2275  r19.41v  3273  r19.41  3274  rabrab  3305  rabrabi  3417  ceqsex3v  3474  spc2ed  3530  ceqsrex2v  3580  rexrab  3626  rexrab2  3632  2reu5  3688  rexss  3988  inass  4150  rexin  4170  indifdirOLD  4216  difin2  4222  difrab  4239  reupick3  4250  inssdif0  4300  rexdifpr  4591  rexdifsn  4724  reusv2lem4  5319  reusv2  5321  eqvinop  5395  copsexgw  5398  copsexg  5399  rabxp  5626  elvvv  5653  resopab2  5933  difxp  6056  mptpreima  6130  resco  6143  coass  6158  dfpo2  6188  frpoind  6230  wfiOLD  6239  imadif  6502  dff1o2  6705  eqfnfv3  6893  f1ossf1o  6982  isoini  7189  f1oiso  7202  oprabidw  7286  oprabid  7287  dfoprab2  7311  mpoeq123  7325  mpomptx  7365  resoprab2  7371  ov3  7413  uniuni  7590  elxp4  7743  elxp5  7744  oprabex3  7793  frxp  7938  rexsupp  7969  brtpos2  8019  oeeui  8395  oeeu  8396  omabs  8441  mapsnend  8780  xpsnen  8796  xpcomco  8802  xpassen  8806  wemapsolem  9239  epfrs  9420  frind  9439  aceq1  9804  dfac5lem1  9810  dfac5lem2  9811  dfac5lem5  9814  kmlem3  9839  kmlem14  9850  pwfseqlem1  10345  ltexpi  10589  ltexprlem4  10726  axaddf  10832  axmulf  10833  rexuz  12567  rexuz2  12568  nnwos  12584  zmin  12613  rexrp  12680  elixx3g  13021  elfz2  13175  preduz  13307  fzind2  13433  hashbclem  14092  resqrex  14890  rlim  15132  divalglem10  16039  divalgb  16041  gcdass  16183  lcmass  16247  isprm2  16315  infpn2  16542  ispos2  17948  issubmndb  18359  issubg3  18688  resscntz  18853  subgdmdprd  19552  dprd2d2  19562  dfrhm2  19876  isassa  20973  aspval2  21012  fvmptnn04if  21906  ntreq0  22136  cmpcov2  22449  llyi  22533  nllyi  22534  ptpjpre1  22630  tx1cn  22668  tx2cn  22669  txtube  22699  txkgen  22711  trfil2  22946  elflim2  23023  cnpflfi  23058  isfcls  23068  cnextcn  23126  istlm  23244  blres  23492  metrest  23586  isnlm  23745  elpi1  24114  isclmp  24166  iscvsp  24197  isncvsngp  24218  iscph  24239  cfilucfil3  24389  itg1climres  24784  itgsubst  25118  ulmdvlem3  25466  cubic  25904  vmasum  26269  lgsquadlem1  26433  lgsquadlem2  26434  legov  26850  perpln1  26975  axcontlem5  27239  nbgrel  27610  nbusgredgeu0  27638  nb3grpr2  27653  finsumvtxdg2ssteplem3  27817  usgr2pth0  28034  isclwlke  28046  wwlksnfi  28172  elwwlks2ons3  28221  wpthswwlks2on  28227  usgr2wspthon  28231  rusgrnumwwlkl1  28234  isclwwlk  28249  isclwwlknx  28301  clwlknf1oclwwlkn  28349  clwwlknonel  28360  clwwlknon2x  28368  clwwlkvbij  28378  iseupthf1o  28467  fusgr2wsp2nb  28599  grpoidinvlem3  28769  h2hlm  29243  issh  29471  issh3  29482  ocsh  29546  cvbr2  30546  cvnbtwn2  30550  mdsl2i  30585  cvmdi  30587  mdsymlem2  30667  sumdmdii  30678  dmrab  30745  difrab2  30746  disjunsn  30834  mpomptxf  30918  ressupprn  30926  1stpreima  30941  2ndpreima  30942  f1od2  30958  nndiffz1  31009  omndmul2  31240  smatrcl  31648  crefdf  31700  1stmbfm  32127  2ndmbfm  32128  dya2iocnei  32149  eulerpartlemgvv  32243  eulerpartlemn  32248  bnj250  32580  bnj251  32581  bnj256  32585  bnj168  32609  cusgr3cyclex  32998  iscvm  33121  axacprim  33548  riotarab  33575  reurab  33576  eldifsucnn  33597  dfdm5  33653  dfrn5  33654  elima4  33656  sltval2  33786  madeval2  33964  dfon3  34121  brimg  34166  dfrecs2  34179  dfrdg4  34180  ifscgr  34273  cgrxfr  34284  segcon2  34334  seglecgr12im  34339  segletr  34343  ellines  34381  neifg  34487  bj-dfmpoa  35216  bj-imdiridlem  35283  bj-imdirco  35288  topdifinffinlem  35445  icorempo  35449  difunieq  35472  finxpreclem6  35494  wl-df4-3mintru2  35585  wl-cases2-dnf  35598  curf  35682  uncf  35683  matunitlindflem2  35701  matunitlindf  35702  poimirlem26  35730  poimirlem28  35732  poimirlem30  35734  poimirlem32  35736  poimir  35737  itg2addnc  35758  ftc1anclem5  35781  ftc1anc  35785  areacirclem5  35796  isbnd2  35868  heibor1  35895  anan  36306  inxpxrn  36448  prtlem70  36798  prtlem100  36800  lsateln0  36936  islshpat  36958  lcvbr2  36963  lcvnbtwn2  36968  isopos  37121  cvrval2  37215  cvrnbtwn2  37216  ishlat2  37294  3dim0  37398  islvol5  37520  pmapjat1  37794  pclcmpatN  37842  pclfinclN  37891  cdlemefrs29pre00  38336  cdlemefrs29bpre0  38337  cdlemefrs29cpre1  38339  cdleme32a  38382  cdlemftr3  38506  dvhopellsm  39058  dibelval3  39088  diblsmopel  39112  mapdvalc  39570  mapdval4N  39573  mapdordlem1a  39575  3factsumint2  39958  3factsumint3  39959  3factsumint4  39960  3factsumint  39961  aks4d1p8  40023  fsuppind  40202  diophrex  40513  rmxdioph  40754  dford4  40767  islmodfg  40810  islssfg2  40812  isdomn3  40945  fgraphopab  40951  k0004lem1  41646  ismnuprim  41801  2sbc5g  41923  limcrecl  43060  dvnmul  43374  dvnprodlem2  43378  fourierdlem83  43620  iundjiun  43888  fcoresf1ob  44454  f1ocof1ob  44460  4an21  44649  sprvalpwn0  44823  pairreueq  44850  prprsprreu  44859  prprreueq  44860  isrnghm  45338  isrnghmmul  45339  rngcinv  45427  rngcinvALTV  45439  ringcinv  45478  ringcinvALTV  45502  mpomptx2  45558  opnneir  46088  opnneilv  46090  i0oii  46101  io1ii  46102  iscnrm3lem3  46117