Theorem anass 472

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 471	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		id 22	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	anasss 470	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	2, 4	impbii 211	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ↔ wb 208   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  bianass  652  an31  658  an4  666  3anass  1107  3an4anass  1118  4anpull2OLD  1377  an33rean  1506  2sb5  2314  r19.41v  3194  r3ex  3203  r19.41  3268  rabrabi  3435  rabrab  3440  ceqsex3v  3508  spc2ed  3562  ceqsrex2v  3619  rexrab  3661  rexrab2  3665  reurab  3666  2reu5  3723  rexssOLD  4014  inass  4181  rexin  4204  difin2  4255  difrab  4272  reupick3  4284  inssdif0  4329  rabsneq  4603  rexdifpr  4620  rexdifsn  4756  reusv2lem4  5360  reusv2  5362  eqvinop  5457  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  rabxp  5697  elvvv  5725  resopab2  6027  difxp  6151  mptpreima  6227  resco  6239  coass  6255  dfpo2  6285  frpoind  6331  imadif  6607  dff1o2  6814  eqfnfv3  7015  f1ossf1o  7112  isoini  7324  f1oiso  7337  riotarab  7397  oprabidw  7429  oprabid  7430  dfoprab2  7456  mpoeq123  7470  mpomptx  7511  resoprab2  7517  ov3  7561  uniuni  7747  elxp4  7905  elxp5  7906  oprabex3  7960  frxp  8108  rexsupp  8164  brtpos2  8214  oeeui  8574  oeeu  8575  omabs  8623  eldifsucnn  8636  naddsuc2  8674  mapsnend  9019  xpsnen  9035  xpcomco  9041  xpassen  9045  wemapsolem  9500  epfrs  9688  frind  9710  aceq1  10075  dfac5lem1  10081  dfac5lem2  10082  dfac5lem5  10085  kmlem3  10111  kmlem14  10122  pwfseqlem1  10618  ltexpi  10862  ltexprlem4  10999  axaddf  11105  axmulf  11106  rexuz  12901  rexuz2  12902  nnwos  12918  zmin  12947  rexrp  13018  elixx3g  13364  elfz2  13521  preduz  13657  fzind2  13796  hashbclem  14467  resqrex  15279  rlim  15524  divalglem10  16438  divalgb  16440  gcdass  16583  lcmass  16650  isprm2  16718  infpn2  16951  ispos2  18349  issubmndb  18841  issubg3  19188  resscntz  19375  subgdmdprd  20078  dprd2d2  20088  omndmul2  20175  isrnghm  20492  isrnghmmul  20493  dfrhm2  20525  rngcinv  20689  ringcinv  20723  isdomn3  20767  aspval2  21952  fvmptnn04if  22911  ntreq0  23139  cmpcov2  23452  llyi  23536  nllyi  23537  ptpjpre1  23633  tx1cn  23671  tx2cn  23672  txtube  23702  txkgen  23714  trfil2  23949  elflim2  24026  cnpflfi  24061  isfcls  24071  cnextcn  24129  istlm  24247  blres  24493  metrest  24586  isnlm  24737  elpi1  25109  isclmp  25161  iscvsp  25192  isncvsngp  25213  iscph  25234  cfilucfil3  25384  itg1climres  25778  itgsubst  26113  ulmdvlem3  26467  cubic  26916  vmasum  27282  lgsquadlem1  27446  lgsquadlem2  27447  ltsval2  27722  madeval2  27928  legov  28756  perpln1  28885  axcontlem5  29171  nbgrel  29543  nbusgredgeu0  29571  nb3grpr2  29586  finsumvtxdg2ssteplem3  29750  usgr2pth0  29967  isclwlke  29979  wwlksnfi  30108  elwwlks2ons3  30157  wpthswwlks2on  30166  usgr2wspthon  30170  rusgrnumwwlkl1  30173  isclwwlk  30188  isclwwlknx  30240  clwlknf1oclwwlkn  30288  clwwlknonel  30299  clwwlknon2x  30307  clwwlkvbij  30317  iseupthf1o  30406  fusgr2wsp2nb  30538  grpoidinvlem3  30711  h2hlm  31185  issh  31413  issh3  31424  ocsh  31488  cvbr2  32488  cvnbtwn2  32492  mdsl2i  32527  cvmdi  32529  mdsymlem2  32609  sumdmdii  32620  dmrab  32698  difrab2  32699  disjunsn  32796  mpomptxf  32882  ressupprn  32894  1stpreima  32911  2ndpreima  32912  f1od2  32923  nndiffz1  32990  1arithufdlem4  33745  r1plmhm  33808  r1pquslmic  33809  extdgfialglem1  33991  smatrcl  34095  crefdf  34147  1stmbfm  34559  2ndmbfm  34560  dya2iocnei  34581  eulerpartlemgvv  34675  eulerpartlemn  34680  bnj250  34999  bnj251  35000  bnj256  35004  bnj168  35028  cusgr3cyclex  35491  iscvm  35614  axacprim  36062  dfdm5  36128  dfrn5  36129  elima4  36131  dfon3  36245  brimg  36290  dfrecs2  36305  dfrdg4  36306  ifscgr  36399  cgrxfr  36410  segcon2  36460  seglecgr12im  36465  segletr  36469  ellines  36507  neifg  36736  bj-axseprep  37564  bj-dfmpoa  37613  bj-imdiridlem  37682  bj-imdirco  37687  topdifinffinlem  37846  icorempo  37850  difunieq  37873  finxpreclem6  37895  wl-df4-3mintru2  37986  wl-cases2-dnf  38020  curf  38102  uncf  38103  matunitlindflem2  38121  matunitlindf  38122  poimirlem26  38150  poimirlem28  38152  poimirlem30  38154  poimirlem32  38156  poimir  38157  itg2addnc  38178  ftc1anclem5  38201  ftc1anc  38205  areacirclem5  38216  isbnd2  38287  heibor1  38314  anan  38739  br1cnvres  38778  inxpxrn  38922  prtlem70  39486  prtlem100  39488  lsateln0  39624  islshpat  39646  lcvbr2  39651  lcvnbtwn2  39656  isopos  39809  cvrval2  39903  cvrnbtwn2  39904  ishlat2  39982  3dim0  40086  islvol5  40208  pmapjat1  40482  pclcmpatN  40530  pclfinclN  40579  cdlemefrs29pre00  41024  cdlemefrs29bpre0  41025  cdlemefrs29cpre1  41027  cdleme32a  41070  cdlemftr3  41194  dvhopellsm  41746  dibelval3  41776  diblsmopel  41800  mapdvalc  42258  mapdval4N  42261  mapdordlem1a  42263  3factsumint2  42644  3factsumint3  42645  3factsumint4  42646  3factsumint  42647  aks4d1p8  42709  redvmptabs  42974  fimgmcyc  43157  fsuppind  43177  diophrex  43361  rmxdioph  43598  dford4  43611  islmodfg  43651  islssfg2  43653  fgraphopab  43785  cantnftermord  43902  tfsconcatlem  43918  k0004lem1  44728  ismnuprim  44875  2sbc5g  44997  modelaxreplem3  45561  limcrecl  46210  dvnmul  46522  dvnprodlem2  46526  fourierdlem83  46768  iundjiun  47039  fcoresf1ob  47672  f1ocof1ob  47680  4an21  47869  sprvalpwn0  48094  pairreueq  48121  prprsprreu  48130  prprreueq  48131  clnbgrel  48455  dfvopnbgr2  48480  rngcinvALTV  48903  ringcinvALTV  48937  mpomptx2  48962  reuxfr1dd  49433  coxp  49459  opnneir  49533  opnneilv  49535  i0oii  49546  io1ii  49547  upfval2  49803