Theorem anass 473

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

Syntax hints:   ↔ wb 209   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  bianass  654  an31  660  an4  668  3anass  1109  3an4anass  1120  4anpull2OLD  1381  an33rean  1511  2sb5  2319  r19.41v  3201  r3ex  3210  r19.41  3275  rabrabi  3442  rabrab  3447  ceqsex3v  3515  spc2ed  3569  ceqsrex2v  3626  rexrab  3668  rexrab2  3672  reurab  3673  2reu5  3730  rexssOLD  4021  inass  4188  rexin  4211  difin2  4262  difrab  4279  reupick3  4291  inssdif0  4337  rabsneq  4613  rexdifpr  4630  rexdifsn  4766  reusv2lem4  5373  reusv2  5375  eqvinop  5470  copsexgw  5473  copsexgwOLD  5474  copsexg  5475  rabxp  5710  elvvv  5738  resopab2  6039  difxp  6162  mptpreima  6240  resco  6252  coass  6268  dfpo2  6298  frpoind  6344  imadif  6621  dff1o2  6827  eqfnfv3  7028  f1ossf1o  7125  isoini  7337  f1oiso  7350  riotarab  7410  oprabidw  7442  oprabid  7443  dfoprab2  7469  mpoeq123  7483  mpomptx  7524  resoprab2  7530  ov3  7574  uniuni  7760  elxp4  7918  elxp5  7919  oprabex3  7973  frxp  8121  rexsupp  8177  brtpos2  8227  oeeui  8587  oeeu  8588  omabs  8636  eldifsucnn  8649  naddsuc2  8687  mapsnend  9032  xpsnen  9048  xpcomco  9054  xpassen  9058  wemapsolem  9511  epfrs  9699  frind  9721  aceq1  10100  dfac5lem1  10106  dfac5lem2  10107  dfac5lem5  10110  kmlem3  10135  kmlem14  10146  pwfseqlem1  10642  ltexpi  10886  ltexprlem4  11023  axaddf  11129  axmulf  11130  rexuz  12921  rexuz2  12922  nnwos  12938  zmin  12967  rexrp  13038  elixx3g  13384  elfz2  13541  preduz  13677  fzind2  13816  hashbclem  14488  resqrex  15300  rlim  15545  divalglem10  16459  divalgb  16461  gcdass  16604  lcmass  16671  isprm2  16739  infpn2  16972  ispos2  18370  issubmndb  18862  issubg3  19210  resscntz  19402  subgdmdprd  20105  dprd2d2  20115  omndmul2  20202  isrnghm  20522  isrnghmmul  20523  dfrhm2  20555  rngcinv  20721  ringcinv  20755  isdomn3  20798  aspval2  22016  fvmptnn04if  22974  ntreq0  23202  cmpcov2  23515  llyi  23599  nllyi  23600  ptpjpre1  23696  tx1cn  23734  tx2cn  23735  txtube  23765  txkgen  23777  trfil2  24012  elflim2  24089  cnpflfi  24124  isfcls  24134  cnextcn  24192  istlm  24310  blres  24556  metrest  24649  isnlm  24800  elpi1  25172  isclmp  25224  iscvsp  25255  isncvsngp  25276  iscph  25297  cfilucfil3  25447  itg1climres  25841  itgsubst  26176  ulmdvlem3  26530  cubic  26979  vmasum  27345  lgsquadlem1  27509  lgsquadlem2  27510  ltsval2  27785  madeval2  27991  legov  28819  perpln1  28948  prlngmolem2  29155  axcontlem5  29258  nbgrel  29630  nbusgredgeu0  29658  nb3grpr2  29673  finsumvtxdg2ssteplem3  29837  usgr2pth0  30054  isclwlke  30066  wwlksnfi  30195  elwwlks2ons3  30244  wpthswwlks2on  30253  usgr2wspthon  30257  rusgrnumwwlkl1  30260  isclwwlk  30275  isclwwlknx  30327  clwlknf1oclwwlkn  30375  clwwlknonel  30386  clwwlknon2x  30394  clwwlkvbij  30404  iseupthf1o  30493  fusgr2wsp2nb  30625  grpoidinvlem3  30798  h2hlm  31272  issh  31500  issh3  31511  ocsh  31575  cvbr2  32575  cvnbtwn2  32579  mdsl2i  32614  cvmdi  32616  mdsymlem2  32696  sumdmdii  32707  dmrab  32783  difrab2  32784  disjunsn  32879  mpomptxf  32963  ressupprn  32975  1stpreima  32992  2ndpreima  32993  f1od2  33004  nndiffz1  33071  1arithufdlem4  33781  r1plmhm  33843  r1pquslmic  33844  extdgfialglem1  34026  smatrcl  34130  crefdf  34182  1stmbfm  34594  2ndmbfm  34595  dya2iocnei  34616  eulerpartlemgvv  34710  eulerpartlemn  34715  bnj250  35034  bnj251  35035  bnj256  35039  bnj168  35063  cusgr3cyclex  35526  iscvm  35649  axacprim  36097  dfdm5  36163  dfrn5  36164  elima4  36166  dfon3  36280  brimg  36325  dfrecs2  36340  dfrdg4  36341  ifscgr  36434  cgrxfr  36445  segcon2  36495  seglecgr12im  36500  segletr  36504  ellines  36542  neifg  36770  bj-axseprep  37598  bj-dfmpoa  37647  bj-imdiridlem  37716  bj-imdirco  37721  topdifinffinlem  37880  icorempo  37884  difunieq  37907  finxpreclem6  37929  wl-df4-3mintru2  38020  wl-cases2-dnf  38054  curf  38136  uncf  38137  matunitlindflem2  38155  matunitlindf  38156  poimirlem26  38184  poimirlem28  38186  poimirlem30  38188  poimirlem32  38190  poimir  38191  itg2addnc  38212  ftc1anclem5  38235  ftc1anc  38239  areacirclem5  38250  isbnd2  38321  heibor1  38348  anan  38773  br1cnvres  38812  inxpxrn  38956  prtlem70  39520  prtlem100  39522  lsateln0  39658  islshpat  39680  lcvbr2  39685  lcvnbtwn2  39690  isopos  39843  cvrval2  39937  cvrnbtwn2  39938  ishlat2  40016  3dim0  40120  islvol5  40242  pmapjat1  40516  pclcmpatN  40564  pclfinclN  40613  cdlemefrs29pre00  41058  cdlemefrs29bpre0  41059  cdlemefrs29cpre1  41061  cdleme32a  41104  cdlemftr3  41228  dvhopellsm  41780  dibelval3  41810  diblsmopel  41834  mapdvalc  42292  mapdval4N  42295  mapdordlem1a  42297  3factsumint2  42678  3factsumint3  42679  3factsumint4  42680  3factsumint  42681  aks4d1p8  42743  redvmptabs  43010  fimgmcyc  43193  fsuppind  43213  diophrex  43397  rmxdioph  43634  dford4  43647  islmodfg  43687  islssfg2  43689  fgraphopab  43821  cantnftermord  43938  tfsconcatlem  43954  k0004lem1  44764  ismnuprim  44895  2sbc5g  45017  modelaxreplem3  45580  limcrecl  46236  dvnmul  46548  dvnprodlem2  46552  fourierdlem83  46794  iundjiun  47065  fcoresf1ob  47698  f1ocof1ob  47706  4an21  47895  sprvalpwn0  48120  pairreueq  48147  prprsprreu  48156  prprreueq  48157  clnbgrel  48481  dfvopnbgr2  48506  rngcinvALTV  48929  ringcinvALTV  48963  mpomptx2  48999  reuxfr1dd  49469  coxp  49495  opnneir  49569  opnneilv  49571  i0oii  49582  io1ii  49583  upfval2  49839