Theorem anass 474

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 23	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
2	1	anassrs 473	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		id 23	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	anasss 472	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	2, 4	impbii 212	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

This proof depends on syntax axioms:   ↔ wb 209   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  bianass  655  an31  661  an4  669  3anass  1111  3an4anass  1122  4anpull2OLD  1383  an33rean  1514  2sb5  2312  r19.41v  3193  r3ex  3202  r19.41  3267  rabrabi  3431  rabrab  3436  ceqsex3v  3503  spc2ed  3556  ceqsrex2v  3612  rexrab  3654  rexrab2  3658  reurab  3659  2reu5  3716  rexssOLD  4007  inass  4173  rexin  4196  difin2  4247  difrab  4264  reupick3  4276  inssdif0OLD  4323  rabsneq  4603  rexdifpr  4620  rexdifsn  4757  reusv2lem4  5363  reusv2  5365  eqvinop  5456  eqvinot  5457  copsexgw  5460  copsexgwOLD  5461  copsexg  5462  cotsexgw  5463  rabxp  5699  elvvv  5727  resopab2  6028  difxp  6155  mptpreima  6239  resco  6251  coass  6267  dfpo2  6299  frpoind  6345  imadif  6624  dff1o2  6830  eqfnfv3  7031  f1ossf1o  7129  isoini  7346  f1oiso  7359  riotarab  7419  oprabidw  7451  oprabid  7452  dfoprab2  7478  mpoeq123  7492  mpomptx  7533  resoprab2  7539  ov3  7583  uniuni  7776  elxp4  7934  elxp5  7935  oprabex3  7989  frxp  8138  rexsupp  8199  brtpos2  8249  oeeui  8611  oeeu  8612  omabs  8660  eldifsucnn  8673  naddsuc2  8711  curf  8890  uncf  8891  mapsnend  9064  xpsnen  9080  xpcomco  9086  xpassen  9090  wemapsolem  9544  epfrs  9732  frind  9754  aceq1  10196  dfac5lem1  10202  dfac5lem2  10203  dfac5lem5  10206  kmlem3  10231  kmlem14  10242  pwfseqlem1  10743  ltexpi  10987  ltexprlem4  11124  axaddf  11230  axmulf  11231  rexuz  13025  rexuz2  13026  nnwos  13042  zmin  13071  rexrp  13143  elixx3g  13489  elfz2  13646  preduz  13784  fzind2  13923  hashbclem  14597  resqrex  15417  rlim  15662  divalglem10  16572  divalgb  16574  gcdass  16720  lcmass  16789  isprm2  16857  infpn2  17091  ispos2  18489  issubmndb  19000  issubg3  19355  resscntz  19547  subgdmdprd  20250  dprd2d2  20260  omndmul2  20347  dfring3  20518  isrnghm  20671  isrnghmmul  20672  dfrhm2  20704  rngcinv  20889  ringcinv  20923  isdomn3  20966  aspval2  22206  matunitlindflem2  22995  matunitlindf  22996  fvmptnn04if  23167  ntreq0  23395  cmpcov2  23708  llyi  23793  nllyi  23794  ptpjpre1  23890  tx1cn  23928  tx2cn  23929  txtube  23959  txkgen  23971  trfil2  24206  elflim2  24283  cnpflfi  24318  isfcls  24328  cnextcn  24386  istlm  24504  blres  24750  metrest  24843  isnlm  24994  elpi1  25366  isclmp  25418  iscvsp  25449  isncvsngp  25470  iscph  25491  cfilucfil3  25641  itg1climres  26035  itgsubst  26369  ulmdvlem3  26729  cubic  27177  vmasum  27543  lgsquadlem1  27707  lgsquadlem2  27708  ltsval2  28013  madeval2  28219  legov  29048  perpln1  29185  prlngmolem2  29431  axcontlem5  29546  nbgrel  29921  nbusgredgeu0  29949  nb3grpr2  29964  finsumvtxdg2ssteplem3  30128  usgr2pth0  30351  isclwlke  30364  wwlksnfi  30495  elwwlks2ons3  30544  wpthswwlks2on  30553  usgr2wspthon  30557  rusgrnumwwlkl1  30560  isclwwlk  30575  isclwwlknx  30627  clwlknf1oclwwlkn  30675  clwwlknonel  30686  clwwlknon2x  30694  clwwlkvbij  30704  iseupthf1o  30803  fusgr2wsp2nb  30935  grpoidinvlem3  31108  h2hlm  31582  issh  31810  issh3  31821  ocsh  31885  cvbr2  32885  cvnbtwn2  32889  mdsl2i  32924  cvmdi  32926  mdsymlem2  33006  sumdmdii  33017  dmrab  33093  difrab2  33094  disjunsn  33188  mpomptxf  33272  ressupprn  33283  1stpreima  33300  2ndpreima  33301  f1od2  33311  nndiffz1  33378  1arithufdlem4  34079  r1plmhm  34141  r1pquslmic  34142  extdgfialglem1  34324  smatrcl  34428  crefdf  34480  1stmbfm  34892  2ndmbfm  34893  dya2iocnei  34914  eulerpartlemgvv  35008  eulerpartlemn  35013  bnj250  35332  bnj251  35333  bnj256  35337  bnj168  35361  cusgr3cyclex  35911  iscvm  36024  axacprim  36472  dfdm5  36537  dfrn5  36538  elima4  36540  dfon3  36654  brimg  36699  dfrecs2  36714  dfrdg4  36715  ifscgr  36809  cgrxfr  36820  segcon2  36870  seglecgr12im  36875  segletr  36879  ellines  36917  neifg  37159  coi1in  37961  bj-axseprep  37990  bj-dfmpoa  38039  bj-imdiridlem  38106  bj-imdirco  38111  topdifinffinlem  38270  icorempo  38274  difunieq  38297  finxpreclem6  38319  wl-df4-3mintru2  38410  wl-cases2-dnf  38444  poimirlem26  38564  poimirlem28  38566  poimirlem30  38568  poimirlem32  38570  poimir  38571  itg2addnc  38592  ftc1anclem5  38615  ftc1anc  38619  areacirclem5  38630  isbnd2  38717  heibor1  38744  anan  39167  br1cnvres  39206  inxpxrn  39350  prtlem70  39914  prtlem100  39916  lsateln0  40052  islshpat  40074  lcvbr2  40079  lcvnbtwn2  40084  isopos  40237  cvrval2  40331  cvrnbtwn2  40332  ishlat2  40410  3dim0  40514  islvol5  40636  pmapjat1  40910  pclcmpatN  40958  pclfinclN  41007  cdlemefrs29pre00  41452  cdlemefrs29bpre0  41453  cdlemefrs29cpre1  41455  cdleme32a  41498  cdlemftr3  41622  dvhopellsm  42174  dibelval3  42204  diblsmopel  42228  mapdvalc  42686  mapdval4N  42689  mapdordlem1a  42691  3factsumint2  43072  3factsumint3  43073  3factsumint4  43074  3factsumint  43075  aks4d1p8  43137  redvmptabs  43411  fimgmcyc  43598  fsuppind  43618  diophrex  43785  rmxdioph  44022  dford4  44035  islmodfg  44070  islssfg2  44072  fgraphopab  44204  cantnftermord  44321  tfsconcatlem  44337  k0004lem1  45146  ismnuprim  45277  2sbc5g  45399  modelaxreplem3  45969  limcrecl  46640  dvnmul  46952  dvnprodlem2  46956  fourierdlem83  47198  iundjiun  47469  fcoresf1ob  48142  f1ocof1ob  48150  4an21  48339  sprvalpwn0  48564  pairreueq  48591  prprsprreu  48600  prprreueq  48601  clnbgrel  48925  dfvopnbgr2  48950  rngcinvALTV  49372  ringcinvALTV  49406  mpomptx2  49446  reuxfr1dd  49916  coxp  49942  opnneir  50014  opnneilv  50016  i0oii  50027  io1ii  50028  upfval2  50284  alsanmo  50905  ralsanmo  50906  2alsraln0  50912