Theorem anass 471

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

Syntax hints:   ↔ wb 208   ∧ wa 398

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 399

This theorem is referenced by:  bianass  640  an31  646  an4  654  3anass  1091  3an4anass  1101  an33rean  1479  2sb5  2282  r19.41v  3349  r19.41  3350  rabrab  3381  ceqsex3v  3547  spc2ed  3604  ceqsrex2v  3653  rexrab  3689  rexrab2  3695  2reu5  3751  rexss  4040  inass  4198  rexin  4218  indifdir  4262  difin2  4268  difrab  4279  reupick3  4290  inssdif0  4331  rexdifpr  4600  rexdifsn  4729  reusv2lem4  5304  reusv2  5306  eqvinop  5380  copsexgw  5383  copsexg  5384  rabxp  5602  elvvv  5629  resopab2  5906  difxp  6023  mptpreima  6094  resco  6105  coass  6120  wfi  6183  imadif  6440  dff1o2  6622  eqfnfv3  6806  f1ossf1o  6892  isoini  7093  f1oiso  7106  oprabidw  7189  oprabid  7190  dfoprab2  7214  mpoeq123  7228  mpomptx  7267  resoprab2  7273  ov3  7313  uniuni  7486  elxp4  7629  elxp5  7630  oprabex3  7680  frxp  7822  rexsupp  7850  brtpos2  7900  oeeui  8230  oeeu  8231  omabs  8276  mapsnend  8590  xpsnen  8603  xpcomco  8609  xpassen  8613  wemapsolem  9016  epfrs  9175  aceq1  9545  dfac5lem1  9551  dfac5lem2  9552  dfac5lem5  9555  kmlem3  9580  kmlem14  9591  pwfseqlem1  10082  ltexpi  10326  ltexprlem4  10463  axaddf  10569  axmulf  10570  rexuz  12301  rexuz2  12302  nnwos  12318  zmin  12347  rexrp  12413  elixx3g  12754  elfz2  12902  preduz  13032  fzind2  13158  hashbclem  13813  resqrex  14612  rlim  14854  divalglem10  15755  divalgb  15757  gcdass  15897  lcmass  15960  isprm2  16028  infpn2  16251  ispos2  17560  issubmndb  17972  issubg3  18299  resscntz  18464  subgdmdprd  19158  dprd2d2  19168  dfrhm2  19471  isassa  20090  aspval2  20129  fvmptnn04if  21459  ntreq0  21687  cmpcov2  22000  llyi  22084  nllyi  22085  ptpjpre1  22181  tx1cn  22219  tx2cn  22220  txtube  22250  txkgen  22262  trfil2  22497  elflim2  22574  cnpflfi  22609  isfcls  22619  cnextcn  22677  istlm  22795  blres  23043  metrest  23136  isnlm  23286  elpi1  23651  isclmp  23703  iscvsp  23734  isncvsngp  23755  iscph  23776  cfilucfil3  23925  itg1climres  24317  itgsubst  24648  ulmdvlem3  24992  cubic  25429  vmasum  25794  lgsquadlem1  25958  lgsquadlem2  25959  legov  26373  perpln1  26498  axcontlem5  26756  nbgrel  27124  nbusgredgeu0  27152  nb3grpr2  27167  finsumvtxdg2ssteplem3  27331  usgr2pth0  27548  isclwlke  27560  wwlksnfi  27686  wwlksnfiOLD  27687  elwwlks2ons3  27736  wpthswwlks2on  27742  usgr2wspthon  27746  rusgrnumwwlkl1  27749  isclwwlk  27764  isclwwlknx  27816  clwlknf1oclwwlkn  27865  clwwlknonel  27876  clwwlknon2x  27884  clwwlkvbij  27894  iseupthf1o  27983  fusgr2wsp2nb  28115  grpoidinvlem3  28285  h2hlm  28759  issh  28987  issh3  28998  ocsh  29062  cvbr2  30062  cvnbtwn2  30066  mdsl2i  30101  cvmdi  30103  mdsymlem2  30183  sumdmdii  30194  dmrab  30262  difrab2  30263  disjunsn  30346  mpomptxf  30427  1stpreima  30444  2ndpreima  30445  f1od2  30459  nndiffz1  30511  omndmul2  30715  smatrcl  31063  crefdf  31114  1stmbfm  31520  2ndmbfm  31521  dya2iocnei  31542  eulerpartlemgvv  31636  eulerpartlemn  31641  bnj250  31973  bnj251  31974  bnj256  31978  bnj168  32002  cusgr3cyclex  32385  iscvm  32508  axacprim  32935  dfpo2  32993  dfdm5  33018  dfrn5  33019  elima4  33021  frpoind  33082  frind  33087  sltval2  33165  madeval2  33292  dfon3  33355  brimg  33400  dfrecs2  33413  dfrdg4  33414  ifscgr  33507  cgrxfr  33518  segcon2  33568  seglecgr12im  33573  segletr  33577  ellines  33615  neifg  33721  bj-dfmpoa  34412  bj-imdirid  34477  topdifinffinlem  34630  icorempo  34634  difunieq  34657  finxpreclem6  34679  wl-cases2-dnf  34754  curf  34872  uncf  34873  matunitlindflem2  34891  matunitlindf  34892  poimirlem26  34920  poimirlem28  34922  poimirlem30  34924  poimirlem32  34926  poimir  34927  itg2addnc  34948  ftc1anclem5  34973  ftc1anc  34977  areacirclem5  34988  isbnd2  35063  heibor1  35090  anan  35501  inxpxrn  35645  prtlem70  35995  prtlem100  35997  lsateln0  36133  islshpat  36155  lcvbr2  36160  lcvnbtwn2  36165  isopos  36318  cvrval2  36412  cvrnbtwn2  36413  ishlat2  36491  3dim0  36595  islvol5  36717  pmapjat1  36991  pclcmpatN  37039  pclfinclN  37088  cdlemefrs29pre00  37533  cdlemefrs29bpre0  37534  cdlemefrs29cpre1  37536  cdleme32a  37579  cdlemftr3  37703  dvhopellsm  38255  dibelval3  38285  diblsmopel  38309  mapdvalc  38767  mapdval4N  38770  mapdordlem1a  38772  diophrex  39379  rmxdioph  39620  dford4  39633  islmodfg  39676  islssfg2  39678  isdomn3  39811  fgraphopab  39817  k0004lem1  40504  ismnuprim  40637  2sbc5g  40755  limcrecl  41917  dvnmul  42235  dvnprodlem2  42239  fourierdlem83  42481  iundjiun  42749  4an21  43476  sprvalpwn0  43652  pairreueq  43679  prprsprreu  43688  prprreueq  43689  isrnghm  44170  isrnghmmul  44171  rngcinv  44259  rngcinvALTV  44271  ringcinv  44310  ringcinvALTV  44334  mpomptx2  44390