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  7761  elxp4  7919  elxp5  7920  oprabex3  7974  frxp  8122  rexsupp  8178  brtpos2  8228  oeeui  8588  oeeu  8589  omabs  8637  eldifsucnn  8650  naddsuc2  8688  mapsnend  9033  xpsnen  9049  xpcomco  9055  xpassen  9059  wemapsolem  9512  epfrs  9700  frind  9722  aceq1  10101  dfac5lem1  10107  dfac5lem2  10108  dfac5lem5  10111  kmlem3  10136  kmlem14  10147  pwfseqlem1  10643  ltexpi  10887  ltexprlem4  11024  axaddf  11130  axmulf  11131  rexuz  12922  rexuz2  12923  nnwos  12939  zmin  12968  rexrp  13039  elixx3g  13385  elfz2  13542  preduz  13678  fzind2  13817  hashbclem  14489  resqrex  15301  rlim  15546  divalglem10  16460  divalgb  16462  gcdass  16605  lcmass  16672  isprm2  16740  infpn2  16973  ispos2  18371  issubmndb  18863  issubg3  19211  resscntz  19403  subgdmdprd  20106  dprd2d2  20116  omndmul2  20203  isrnghm  20523  isrnghmmul  20524  dfrhm2  20556  rngcinv  20722  ringcinv  20756  isdomn3  20799  aspval2  22017  fvmptnn04if  22975  ntreq0  23203  cmpcov2  23516  llyi  23600  nllyi  23601  ptpjpre1  23697  tx1cn  23735  tx2cn  23736  txtube  23766  txkgen  23778  trfil2  24013  elflim2  24090  cnpflfi  24125  isfcls  24135  cnextcn  24193  istlm  24311  blres  24557  metrest  24650  isnlm  24801  elpi1  25173  isclmp  25225  iscvsp  25256  isncvsngp  25277  iscph  25298  cfilucfil3  25448  itg1climres  25842  itgsubst  26177  ulmdvlem3  26531  cubic  26980  vmasum  27346  lgsquadlem1  27510  lgsquadlem2  27511  ltsval2  27786  madeval2  27992  legov  28820  perpln1  28949  prlngmolem2  29156  axcontlem5  29259  nbgrel  29631  nbusgredgeu0  29659  nb3grpr2  29674  finsumvtxdg2ssteplem3  29838  usgr2pth0  30055  isclwlke  30067  wwlksnfi  30196  elwwlks2ons3  30245  wpthswwlks2on  30254  usgr2wspthon  30258  rusgrnumwwlkl1  30261  isclwwlk  30276  isclwwlknx  30328  clwlknf1oclwwlkn  30376  clwwlknonel  30387  clwwlknon2x  30395  clwwlkvbij  30405  iseupthf1o  30494  fusgr2wsp2nb  30626  grpoidinvlem3  30799  h2hlm  31273  issh  31501  issh3  31512  ocsh  31576  cvbr2  32576  cvnbtwn2  32580  mdsl2i  32615  cvmdi  32617  mdsymlem2  32697  sumdmdii  32708  dmrab  32784  difrab2  32785  disjunsn  32880  mpomptxf  32964  ressupprn  32976  1stpreima  32993  2ndpreima  32994  f1od2  33005  nndiffz1  33072  1arithufdlem4  33782  r1plmhm  33844  r1pquslmic  33845  extdgfialglem1  34027  smatrcl  34131  crefdf  34183  1stmbfm  34595  2ndmbfm  34596  dya2iocnei  34617  eulerpartlemgvv  34711  eulerpartlemn  34716  bnj250  35035  bnj251  35036  bnj256  35040  bnj168  35064  cusgr3cyclex  35561  iscvm  35684  axacprim  36132  dfdm5  36198  dfrn5  36199  elima4  36201  dfon3  36315  brimg  36360  dfrecs2  36375  dfrdg4  36376  ifscgr  36469  cgrxfr  36480  segcon2  36530  seglecgr12im  36535  segletr  36539  ellines  36577  neifg  36805  bj-axseprep  37633  bj-dfmpoa  37682  bj-imdiridlem  37751  bj-imdirco  37756  topdifinffinlem  37915  icorempo  37919  difunieq  37942  finxpreclem6  37964  wl-df4-3mintru2  38055  wl-cases2-dnf  38089  curf  38171  uncf  38172  matunitlindflem2  38190  matunitlindf  38191  poimirlem26  38219  poimirlem28  38221  poimirlem30  38223  poimirlem32  38225  poimir  38226  itg2addnc  38247  ftc1anclem5  38270  ftc1anc  38274  areacirclem5  38285  isbnd2  38356  heibor1  38383  anan  38808  br1cnvres  38847  inxpxrn  38991  prtlem70  39555  prtlem100  39557  lsateln0  39693  islshpat  39715  lcvbr2  39720  lcvnbtwn2  39725  isopos  39878  cvrval2  39972  cvrnbtwn2  39973  ishlat2  40051  3dim0  40155  islvol5  40277  pmapjat1  40551  pclcmpatN  40599  pclfinclN  40648  cdlemefrs29pre00  41093  cdlemefrs29bpre0  41094  cdlemefrs29cpre1  41096  cdleme32a  41139  cdlemftr3  41263  dvhopellsm  41815  dibelval3  41845  diblsmopel  41869  mapdvalc  42327  mapdval4N  42330  mapdordlem1a  42332  3factsumint2  42713  3factsumint3  42714  3factsumint4  42715  3factsumint  42716  aks4d1p8  42778  redvmptabs  43045  fimgmcyc  43228  fsuppind  43248  diophrex  43432  rmxdioph  43669  dford4  43682  islmodfg  43722  islssfg2  43724  fgraphopab  43856  cantnftermord  43973  tfsconcatlem  43989  k0004lem1  44799  ismnuprim  44930  2sbc5g  45052  modelaxreplem3  45615  limcrecl  46271  dvnmul  46583  dvnprodlem2  46587  fourierdlem83  46829  iundjiun  47100  fcoresf1ob  47733  f1ocof1ob  47741  4an21  47930  sprvalpwn0  48155  pairreueq  48182  prprsprreu  48191  prprreueq  48192  clnbgrel  48516  dfvopnbgr2  48541  rngcinvALTV  48964  ringcinvALTV  48998  mpomptx2  49034  reuxfr1dd  49504  coxp  49530  opnneir  49604  opnneilv  49606  i0oii  49617  io1ii  49618  upfval2  49874