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  3174  r3ex  3183  r19.41  3246  rabrabi  3435  rabrab  3440  ceqsex3v  3516  spc2ed  3580  ceqsrex2v  3637  rexrab  3679  rexrab2  3683  reurab  3684  2reu5  3741  rexssOLD  4036  inass  4203  rexin  4225  difin2  4276  difrab  4293  reupick3  4305  inssdif0  4349  rabsneq  4620  rexdifpr  4635  rexdifsn  4770  reusv2lem4  5371  reusv2  5373  eqvinop  5462  copsexgw  5465  copsexg  5466  rabxp  5702  elvvv  5730  resopab2  6023  difxp  6153  mptpreima  6227  resco  6239  coass  6254  dfpo2  6285  frpoind  6331  wfiOLD  6340  imadif  6619  dff1o2  6822  eqfnfv3  7022  f1ossf1o  7117  isoini  7330  f1oiso  7343  riotarab  7402  oprabidw  7434  oprabid  7435  dfoprab2  7463  mpoeq123  7477  mpomptx  7518  resoprab2  7524  ov3  7568  uniuni  7754  elxp4  7916  elxp5  7917  oprabex3  7974  frxp  8123  rexsupp  8179  brtpos2  8229  oeeui  8612  oeeu  8613  omabs  8661  eldifsucnn  8674  naddsuc2  8711  mapsnend  9048  xpsnen  9067  xpcomco  9074  xpassen  9078  wemapsolem  9562  epfrs  9743  frind  9762  aceq1  10129  dfac5lem1  10135  dfac5lem2  10136  dfac5lem5  10139  kmlem3  10165  kmlem14  10176  pwfseqlem1  10670  ltexpi  10914  ltexprlem4  11051  axaddf  11157  axmulf  11158  rexuz  12912  rexuz2  12913  nnwos  12929  zmin  12958  rexrp  13028  elixx3g  13373  elfz2  13529  preduz  13665  fzind2  13799  hashbclem  14468  resqrex  15267  rlim  15509  divalglem10  16419  divalgb  16421  gcdass  16564  lcmass  16631  isprm2  16699  infpn2  16931  ispos2  18325  issubmndb  18781  issubg3  19125  resscntz  19314  subgdmdprd  20015  dprd2d2  20025  isrnghm  20399  isrnghmmul  20400  dfrhm2  20432  rngcinv  20595  ringcinv  20629  isdomn3  20673  aspval2  21856  fvmptnn04if  22785  ntreq0  23013  cmpcov2  23326  llyi  23410  nllyi  23411  ptpjpre1  23507  tx1cn  23545  tx2cn  23546  txtube  23576  txkgen  23588  trfil2  23823  elflim2  23900  cnpflfi  23935  isfcls  23945  cnextcn  24003  istlm  24121  blres  24368  metrest  24461  isnlm  24612  elpi1  24994  isclmp  25046  iscvsp  25077  isncvsngp  25099  iscph  25120  cfilucfil3  25270  itg1climres  25665  itgsubst  26006  ulmdvlem3  26361  cubic  26809  vmasum  27177  lgsquadlem1  27341  lgsquadlem2  27342  sltval2  27618  madeval2  27809  legov  28510  perpln1  28635  axcontlem5  28893  nbgrel  29265  nbusgredgeu0  29293  nb3grpr2  29308  finsumvtxdg2ssteplem3  29473  usgr2pth0  29693  isclwlke  29705  wwlksnfi  29834  elwwlks2ons3  29883  wpthswwlks2on  29889  usgr2wspthon  29893  rusgrnumwwlkl1  29896  isclwwlk  29911  isclwwlknx  29963  clwlknf1oclwwlkn  30011  clwwlknonel  30022  clwwlknon2x  30030  clwwlkvbij  30040  iseupthf1o  30129  fusgr2wsp2nb  30261  grpoidinvlem3  30433  h2hlm  30907  issh  31135  issh3  31146  ocsh  31210  cvbr2  32210  cvnbtwn2  32214  mdsl2i  32249  cvmdi  32251  mdsymlem2  32331  sumdmdii  32342  dmrab  32424  difrab2  32425  disjunsn  32521  mpomptxf  32601  ressupprn  32613  1stpreima  32630  2ndpreima  32631  f1od2  32644  nndiffz1  32709  omndmul2  33026  1arithufdlem4  33508  r1plmhm  33565  r1pquslmic  33566  smatrcl  33773  crefdf  33825  1stmbfm  34238  2ndmbfm  34239  dya2iocnei  34260  eulerpartlemgvv  34354  eulerpartlemn  34359  bnj250  34678  bnj251  34679  bnj256  34683  bnj168  34707  cusgr3cyclex  35104  iscvm  35227  axacprim  35670  dfdm5  35736  dfrn5  35737  elima4  35739  dfon3  35856  brimg  35901  dfrecs2  35914  dfrdg4  35915  ifscgr  36008  cgrxfr  36019  segcon2  36069  seglecgr12im  36074  segletr  36078  ellines  36116  neifg  36335  bj-dfmpoa  37082  bj-imdiridlem  37149  bj-imdirco  37154  topdifinffinlem  37311  icorempo  37315  difunieq  37338  finxpreclem6  37360  wl-df4-3mintru2  37451  wl-cases2-dnf  37476  curf  37568  uncf  37569  matunitlindflem2  37587  matunitlindf  37588  poimirlem26  37616  poimirlem28  37618  poimirlem30  37620  poimirlem32  37622  poimir  37623  itg2addnc  37644  ftc1anclem5  37667  ftc1anc  37671  areacirclem5  37682  isbnd2  37753  heibor1  37780  anan  38193  br1cnvres  38233  inxpxrn  38359  prtlem70  38821  prtlem100  38823  lsateln0  38959  islshpat  38981  lcvbr2  38986  lcvnbtwn2  38991  isopos  39144  cvrval2  39238  cvrnbtwn2  39239  ishlat2  39317  3dim0  39422  islvol5  39544  pmapjat1  39818  pclcmpatN  39866  pclfinclN  39915  cdlemefrs29pre00  40360  cdlemefrs29bpre0  40361  cdlemefrs29cpre1  40363  cdleme32a  40406  cdlemftr3  40530  dvhopellsm  41082  dibelval3  41112  diblsmopel  41136  mapdvalc  41594  mapdval4N  41597  mapdordlem1a  41599  3factsumint2  41981  3factsumint3  41982  3factsumint4  41983  3factsumint  41984  aks4d1p8  42046  redvmptabs  42350  fimgmcyc  42504  fsuppind  42560  diophrex  42745  rmxdioph  42987  dford4  43000  islmodfg  43040  islssfg2  43042  fgraphopab  43174  cantnftermord  43291  tfsconcatlem  43307  k0004lem1  44118  ismnuprim  44266  2sbc5g  44388  modelaxreplem3  44953  limcrecl  45606  dvnmul  45920  dvnprodlem2  45924  fourierdlem83  46166  iundjiun  46437  fcoresf1ob  47050  f1ocof1ob  47058  4an21  47247  sprvalpwn0  47445  pairreueq  47472  prprsprreu  47481  prprreueq  47482  clnbgrel  47790  dfvopnbgr2  47814  rngcinvALTV  48199  ringcinvALTV  48233  mpomptx2  48258  reuxfr1dd  48733  coxp  48759  opnneir  48829  opnneilv  48831  i0oii  48842  io1ii  48843  upfval2  49060