Theorem anass 468

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

Syntax hints:   ↔ wb 206   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  bianass  642  an31  648  an4  656  3anass  1094  3an4anass  1104  4anpull2  1362  an33rean  1485  2sb5  2278  r19.41v  3168  r3ex  3177  r19.41  3242  rabrabi  3428  rabrab  3433  ceqsex3v  3506  spc2ed  3570  ceqsrex2v  3627  rexrab  3670  rexrab2  3674  reurab  3675  2reu5  3732  rexssOLD  4027  inass  4194  rexin  4216  difin2  4267  difrab  4284  reupick3  4296  inssdif0  4340  rabsneq  4611  rexdifpr  4626  rexdifsn  4761  reusv2lem4  5359  reusv2  5361  eqvinop  5450  copsexgw  5453  copsexg  5454  rabxp  5689  elvvv  5717  resopab2  6010  difxp  6140  mptpreima  6214  resco  6226  coass  6241  dfpo2  6272  frpoind  6318  imadif  6603  dff1o2  6808  eqfnfv3  7008  f1ossf1o  7103  isoini  7316  f1oiso  7329  riotarab  7389  oprabidw  7421  oprabid  7422  dfoprab2  7450  mpoeq123  7464  mpomptx  7505  resoprab2  7511  ov3  7555  uniuni  7741  elxp4  7901  elxp5  7902  oprabex3  7959  frxp  8108  rexsupp  8164  brtpos2  8214  oeeui  8569  oeeu  8570  omabs  8618  eldifsucnn  8631  naddsuc2  8668  mapsnend  9010  xpsnen  9029  xpcomco  9036  xpassen  9040  wemapsolem  9510  epfrs  9691  frind  9710  aceq1  10077  dfac5lem1  10083  dfac5lem2  10084  dfac5lem5  10087  kmlem3  10113  kmlem14  10124  pwfseqlem1  10618  ltexpi  10862  ltexprlem4  10999  axaddf  11105  axmulf  11106  rexuz  12864  rexuz2  12865  nnwos  12881  zmin  12910  rexrp  12981  elixx3g  13326  elfz2  13482  preduz  13618  fzind2  13753  hashbclem  14424  resqrex  15223  rlim  15468  divalglem10  16379  divalgb  16381  gcdass  16524  lcmass  16591  isprm2  16659  infpn2  16891  ispos2  18283  issubmndb  18739  issubg3  19083  resscntz  19272  subgdmdprd  19973  dprd2d2  19983  isrnghm  20357  isrnghmmul  20358  dfrhm2  20390  rngcinv  20553  ringcinv  20587  isdomn3  20631  aspval2  21814  fvmptnn04if  22743  ntreq0  22971  cmpcov2  23284  llyi  23368  nllyi  23369  ptpjpre1  23465  tx1cn  23503  tx2cn  23504  txtube  23534  txkgen  23546  trfil2  23781  elflim2  23858  cnpflfi  23893  isfcls  23903  cnextcn  23961  istlm  24079  blres  24326  metrest  24419  isnlm  24570  elpi1  24952  isclmp  25004  iscvsp  25035  isncvsngp  25056  iscph  25077  cfilucfil3  25227  itg1climres  25622  itgsubst  25963  ulmdvlem3  26318  cubic  26766  vmasum  27134  lgsquadlem1  27298  lgsquadlem2  27299  sltval2  27575  madeval2  27768  legov  28519  perpln1  28644  axcontlem5  28902  nbgrel  29274  nbusgredgeu0  29302  nb3grpr2  29317  finsumvtxdg2ssteplem3  29482  usgr2pth0  29702  isclwlke  29714  wwlksnfi  29843  elwwlks2ons3  29892  wpthswwlks2on  29898  usgr2wspthon  29902  rusgrnumwwlkl1  29905  isclwwlk  29920  isclwwlknx  29972  clwlknf1oclwwlkn  30020  clwwlknonel  30031  clwwlknon2x  30039  clwwlkvbij  30049  iseupthf1o  30138  fusgr2wsp2nb  30270  grpoidinvlem3  30442  h2hlm  30916  issh  31144  issh3  31155  ocsh  31219  cvbr2  32219  cvnbtwn2  32223  mdsl2i  32258  cvmdi  32260  mdsymlem2  32340  sumdmdii  32351  dmrab  32433  difrab2  32434  disjunsn  32530  mpomptxf  32608  ressupprn  32620  1stpreima  32637  2ndpreima  32638  f1od2  32651  nndiffz1  32716  omndmul2  33033  1arithufdlem4  33525  r1plmhm  33582  r1pquslmic  33583  smatrcl  33793  crefdf  33845  1stmbfm  34258  2ndmbfm  34259  dya2iocnei  34280  eulerpartlemgvv  34374  eulerpartlemn  34379  bnj250  34698  bnj251  34699  bnj256  34703  bnj168  34727  cusgr3cyclex  35130  iscvm  35253  axacprim  35701  dfdm5  35767  dfrn5  35768  elima4  35770  dfon3  35887  brimg  35932  dfrecs2  35945  dfrdg4  35946  ifscgr  36039  cgrxfr  36050  segcon2  36100  seglecgr12im  36105  segletr  36109  ellines  36147  neifg  36366  bj-dfmpoa  37113  bj-imdiridlem  37180  bj-imdirco  37185  topdifinffinlem  37342  icorempo  37346  difunieq  37369  finxpreclem6  37391  wl-df4-3mintru2  37482  wl-cases2-dnf  37507  curf  37599  uncf  37600  matunitlindflem2  37618  matunitlindf  37619  poimirlem26  37647  poimirlem28  37649  poimirlem30  37651  poimirlem32  37653  poimir  37654  itg2addnc  37675  ftc1anclem5  37698  ftc1anc  37702  areacirclem5  37713  isbnd2  37784  heibor1  37811  anan  38224  br1cnvres  38265  inxpxrn  38388  prtlem70  38857  prtlem100  38859  lsateln0  38995  islshpat  39017  lcvbr2  39022  lcvnbtwn2  39027  isopos  39180  cvrval2  39274  cvrnbtwn2  39275  ishlat2  39353  3dim0  39458  islvol5  39580  pmapjat1  39854  pclcmpatN  39902  pclfinclN  39951  cdlemefrs29pre00  40396  cdlemefrs29bpre0  40397  cdlemefrs29cpre1  40399  cdleme32a  40442  cdlemftr3  40566  dvhopellsm  41118  dibelval3  41148  diblsmopel  41172  mapdvalc  41630  mapdval4N  41633  mapdordlem1a  41635  3factsumint2  42017  3factsumint3  42018  3factsumint4  42019  3factsumint  42020  aks4d1p8  42082  redvmptabs  42355  fimgmcyc  42529  fsuppind  42585  diophrex  42770  rmxdioph  43012  dford4  43025  islmodfg  43065  islssfg2  43067  fgraphopab  43199  cantnftermord  43316  tfsconcatlem  43332  k0004lem1  44143  ismnuprim  44290  2sbc5g  44412  modelaxreplem3  44977  limcrecl  45634  dvnmul  45948  dvnprodlem2  45952  fourierdlem83  46194  iundjiun  46465  fcoresf1ob  47078  f1ocof1ob  47086  4an21  47275  sprvalpwn0  47488  pairreueq  47515  prprsprreu  47524  prprreueq  47525  clnbgrel  47833  dfvopnbgr2  47857  rngcinvALTV  48268  ringcinvALTV  48302  mpomptx2  48327  reuxfr1dd  48799  coxp  48825  opnneir  48899  opnneilv  48901  i0oii  48912  io1ii  48913  upfval2  49170