Theorem anass 462

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

Syntax hints:   ↔ wb 198   ∧ wa 386

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 199  df-an 387

This theorem is referenced by:  bianass  632  an21  634  an12  635  an32  636  an13  637  an31  638  an4  646  3anass  1079  3an4anass  1092  2sb5  2252  eu6OLD  2594  r19.41v  3275  r19.41  3276  rabrab  3303  ceqsex3v  3448  ceqsrex2v  3541  rexrab  3580  rexrab2  3584  2reu5  3633  rexss  3890  inass  4044  rexin  4064  indifdir  4110  difin2  4116  difrab  4127  reupick3  4138  inssdif0  4178  rexdifpr  4427  rexdifsn  4556  reusv2lem4  5113  reusv2  5115  eqvinop  5186  copsexg  5187  rabxp  5400  elvvv  5424  resopab2  5698  difxp  5812  mptpreima  5882  resco  5893  coass  5908  wfi  5966  imadif  6218  dff1o2  6396  eqfnfv3  6576  f1ossf1o  6660  isoini  6860  f1oiso  6873  oprabid  6953  dfoprab2  6978  mpt2eq123  6991  mpt2mptx  7028  resoprab2  7034  ov3  7074  uniuni  7248  elxp4  7389  elxp5  7390  oprabex3  7434  frxp  7568  rexsupp  7594  brtpos2  7640  oeeui  7966  oeeu  7967  omabs  8011  mapsnend  8320  xpsnen  8332  xpcomco  8338  xpassen  8342  wemapsolem  8744  epfrs  8904  aceq1  9273  dfac5lem1  9279  dfac5lem2  9280  dfac5lem5  9283  kmlem3  9309  kmlem14  9320  pwfseqlem1  9815  ltexpi  10059  ltexprlem4  10196  axaddf  10302  axmulf  10303  rexuz  12044  rexuz2  12045  nnwos  12062  zmin  12091  rexrp  12160  elixx3g  12500  elfz2  12650  preduz  12780  fzind2  12905  hashbclem  13550  resqrex  14398  rlim  14634  divalglem10  15532  divalgb  15534  gcdass  15670  lcmass  15733  isprm2  15800  infpn2  16021  ispos2  17334  issubg3  17996  resscntz  18147  subgdmdprd  18820  dprd2d2  18830  dfrhm2  19106  isassa  19712  aspval2  19744  fvmptnn04if  21061  ntreq0  21289  cmpcov2  21602  llyi  21686  nllyi  21687  subislly  21693  ptpjpre1  21783  tx1cn  21821  tx2cn  21822  txtube  21852  txkgen  21864  trfil2  22099  elflim2  22176  cnpflfi  22211  isfcls  22221  cnextcn  22279  istlm  22396  blres  22644  metrest  22737  isnlm  22887  elcncf1di  23106  elpi1  23252  isclmp  23304  iscvsp  23335  isncvsngp  23356  iscph  23377  cfilucfil3  23526  itg1climres  23918  itgsubst  24249  ulmdvlem3  24593  cubic  25027  vmasum  25393  logfac2  25394  lgsquadlem1  25557  lgsquadlem2  25558  legov  25936  perpln1  26061  axcontlem5  26317  nbgrel  26687  nbusgredgeu0  26716  nb3grpr2  26731  finsumvtxdg2ssteplem3  26895  usgr2pth0  27117  isclwlke  27129  wwlksnfi  27278  wwlksnfiOLD  27279  wlksnwwlknvbijOLD  27282  elwwlks2ons3  27335  wpthswwlks2on  27341  usgr2wspthon  27345  rusgrnumwwlkl1  27348  isclwwlk  27364  isclwwlknx  27425  clwlknf1oclwwlkn  27483  clwlknf1oclwwlknOLD  27485  clwwlknonel  27497  clwwlknon2x  27505  clwwlkvbij  27515  clwwlkvbijOLD  27516  iseupthf1o  27605  fusgr2wsp2nb  27742  grpoidinvlem3  27933  h2hlm  28409  issh  28637  issh3  28648  ocsh  28714  cvbr2  29714  cvnbtwn2  29718  mdsl2i  29753  cvmdi  29755  mdsymlem2  29835  sumdmdii  29846  spc2ed  29884  difrab2  29901  disjunsn  29970  mpt2mptxf  30043  1stpreima  30050  2ndpreima  30051  f1od2  30065  nndiffz1  30112  omndmul2  30274  smatrcl  30460  crefdf  30513  pcmplfin  30525  1stmbfm  30920  2ndmbfm  30921  dya2iocnei  30942  eulerpartlemgvv  31036  eulerpartlemn  31041  bnj250  31369  bnj251  31370  bnj256  31374  bnj168  31398  iscvm  31840  axacprim  32181  dfpo2  32239  dfdm5  32264  dfrn5  32265  elima4  32267  imaindm  32270  frpoind  32329  frind  32332  sltval2  32398  madeval2  32525  dfon3  32588  brimg  32633  dfrecs2  32646  dfrdg4  32647  ifscgr  32740  cgrxfr  32751  segcon2  32801  seglecgr12im  32806  segletr  32810  ellines  32848  neifg  32954  bj-dfmpt2a  33644  topdifinffinlem  33790  icorempt2  33794  finxpreclem6  33828  wl-cases2-dnf  33890  curf  34014  uncf  34015  matunitlindflem2  34034  matunitlindf  34035  poimirlem26  34063  poimirlem28  34065  poimirlem30  34067  poimirlem32  34069  poimir  34070  itg2addnc  34091  ftc1anclem5  34116  ftc1anc  34120  areacirclem5  34131  isbnd2  34208  heibor1  34235  anan  34639  inxpxrn  34783  prtlem70  35013  prtlem100  35015  lsateln0  35151  islshpat  35173  lcvbr2  35178  lcvnbtwn2  35183  isopos  35336  cvrval2  35430  cvrnbtwn2  35431  ishlat2  35509  3dim0  35613  islvol5  35735  pmapjat1  36009  pclcmpatN  36057  pclfinclN  36106  cdlemefrs29pre00  36551  cdlemefrs29bpre0  36552  cdlemefrs29cpre1  36554  cdleme32a  36597  cdlemftr3  36721  dvhopellsm  37273  dibelval3  37303  diblsmopel  37327  mapdvalc  37785  mapdval4N  37788  mapdordlem1a  37790  diophrex  38303  rmxdioph  38546  dford4  38559  islmodfg  38602  islssfg2  38604  isdomn3  38745  fgraphopab  38751  k0004lem1  39405  2sbc5g  39576  limcrecl  40773  dvnmul  41090  dvnprodlem2  41094  fourierdlem83  41337  iundjiun  41605  4an21  42315  sprvalpwn0  42426  pairreueq  42453  prprsprreu  42462  prprreueq  42463  isrnghm  42911  isrnghmmul  42912  rngcinv  43000  rngcinvALTV  43012  ringcinv  43051  ringcinvALTV  43075  mpt2mptx2  43132