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  2281  r19.41v  3350  r19.41  3351  rabrab  3382  ceqsex3v  3548  spc2ed  3605  ceqsrex2v  3654  rexrab  3690  rexrab2  3696  2reu5  3752  rexss  4041  inass  4199  rexin  4219  indifdir  4263  difin2  4269  difrab  4280  reupick3  4291  inssdif0  4332  rexdifpr  4601  rexdifsn  4730  reusv2lem4  5305  reusv2  5307  eqvinop  5381  copsexgw  5384  copsexg  5385  rabxp  5603  elvvv  5630  resopab2  5907  difxp  6024  mptpreima  6095  resco  6106  coass  6121  wfi  6184  imadif  6441  dff1o2  6623  eqfnfv3  6807  f1ossf1o  6893  isoini  7094  f1oiso  7107  oprabidw  7190  oprabid  7191  dfoprab2  7215  mpoeq123  7229  mpomptx  7268  resoprab2  7274  ov3  7314  uniuni  7487  elxp4  7630  elxp5  7631  oprabex3  7681  frxp  7823  rexsupp  7851  brtpos2  7901  oeeui  8231  oeeu  8232  omabs  8277  mapsnend  8591  xpsnen  8604  xpcomco  8610  xpassen  8614  wemapsolem  9017  epfrs  9176  aceq1  9546  dfac5lem1  9552  dfac5lem2  9553  dfac5lem5  9556  kmlem3  9581  kmlem14  9592  pwfseqlem1  10083  ltexpi  10327  ltexprlem4  10464  axaddf  10570  axmulf  10571  rexuz  12301  rexuz2  12302  nnwos  12318  zmin  12347  rexrp  12413  elixx3g  12754  elfz2  12902  preduz  13032  fzind2  13158  hashbclem  13813  resqrex  14613  rlim  14855  divalglem10  15756  divalgb  15758  gcdass  15898  lcmass  15961  isprm2  16029  infpn2  16252  ispos2  17561  issubmndb  17973  issubg3  18300  resscntz  18465  subgdmdprd  19159  dprd2d2  19169  dfrhm2  19472  isassa  20091  aspval2  20130  fvmptnn04if  21460  ntreq0  21688  cmpcov2  22001  llyi  22085  nllyi  22086  ptpjpre1  22182  tx1cn  22220  tx2cn  22221  txtube  22251  txkgen  22263  trfil2  22498  elflim2  22575  cnpflfi  22610  isfcls  22620  cnextcn  22678  istlm  22796  blres  23044  metrest  23137  isnlm  23287  elpi1  23652  isclmp  23704  iscvsp  23735  isncvsngp  23756  iscph  23777  cfilucfil3  23926  itg1climres  24318  itgsubst  24649  ulmdvlem3  24993  cubic  25430  vmasum  25795  lgsquadlem1  25959  lgsquadlem2  25960  legov  26374  perpln1  26499  axcontlem5  26757  nbgrel  27125  nbusgredgeu0  27153  nb3grpr2  27168  finsumvtxdg2ssteplem3  27332  usgr2pth0  27549  isclwlke  27561  wwlksnfi  27687  wwlksnfiOLD  27688  elwwlks2ons3  27737  wpthswwlks2on  27743  usgr2wspthon  27747  rusgrnumwwlkl1  27750  isclwwlk  27765  isclwwlknx  27817  clwlknf1oclwwlkn  27866  clwwlknonel  27877  clwwlknon2x  27885  clwwlkvbij  27895  iseupthf1o  27984  fusgr2wsp2nb  28116  grpoidinvlem3  28286  h2hlm  28760  issh  28988  issh3  28999  ocsh  29063  cvbr2  30063  cvnbtwn2  30067  mdsl2i  30102  cvmdi  30104  mdsymlem2  30184  sumdmdii  30195  dmrab  30263  difrab2  30264  disjunsn  30347  mpomptxf  30428  1stpreima  30445  2ndpreima  30446  f1od2  30460  nndiffz1  30512  omndmul2  30717  smatrcl  31065  crefdf  31116  1stmbfm  31522  2ndmbfm  31523  dya2iocnei  31544  eulerpartlemgvv  31638  eulerpartlemn  31643  bnj250  31975  bnj251  31976  bnj256  31980  bnj168  32004  cusgr3cyclex  32387  iscvm  32510  axacprim  32937  dfpo2  32995  dfdm5  33020  dfrn5  33021  elima4  33023  frpoind  33084  frind  33089  sltval2  33167  madeval2  33294  dfon3  33357  brimg  33402  dfrecs2  33415  dfrdg4  33416  ifscgr  33509  cgrxfr  33520  segcon2  33570  seglecgr12im  33575  segletr  33579  ellines  33617  neifg  33723  bj-dfmpoa  34414  bj-imdirid  34479  topdifinffinlem  34632  icorempo  34636  difunieq  34659  finxpreclem6  34681  wl-cases2-dnf  34756  curf  34874  uncf  34875  matunitlindflem2  34893  matunitlindf  34894  poimirlem26  34922  poimirlem28  34924  poimirlem30  34926  poimirlem32  34928  poimir  34929  itg2addnc  34950  ftc1anclem5  34975  ftc1anc  34979  areacirclem5  34990  isbnd2  35065  heibor1  35092  anan  35503  inxpxrn  35647  prtlem70  35997  prtlem100  35999  lsateln0  36135  islshpat  36157  lcvbr2  36162  lcvnbtwn2  36167  isopos  36320  cvrval2  36414  cvrnbtwn2  36415  ishlat2  36493  3dim0  36597  islvol5  36719  pmapjat1  36993  pclcmpatN  37041  pclfinclN  37090  cdlemefrs29pre00  37535  cdlemefrs29bpre0  37536  cdlemefrs29cpre1  37538  cdleme32a  37581  cdlemftr3  37705  dvhopellsm  38257  dibelval3  38287  diblsmopel  38311  mapdvalc  38769  mapdval4N  38772  mapdordlem1a  38774  diophrex  39378  rmxdioph  39619  dford4  39632  islmodfg  39675  islssfg2  39677  isdomn3  39810  fgraphopab  39816  k0004lem1  40503  ismnuprim  40636  2sbc5g  40754  limcrecl  41916  dvnmul  42234  dvnprodlem2  42238  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