Theorem anass 401

Description: Associative law for conjunction. Theorem *4.32 of [WhiteheadRussell] p. 118. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Assertion

Ref	Expression
anass	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Proof of Theorem anass

Step	Hyp	Ref	Expression
1		id 19	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
2	1	anassrs 400	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		id 19	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	anasss 399	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	2, 4	impbii 126	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ∧ wa 104   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  bianass  469  mpan10  474  an12  561  an32  562  an13  563  an31  564  an4  586  3anass  984  sbidm  1865  4exdistr  1931  2sb5  2002  2sb5rf  2008  sbel2x  2017  r2exf  2515  r19.41  2652  ceqsex3v  2806  ceqsrex2v  2896  rexrab  2927  rexrab2  2931  rexss  3251  inass  3374  difin2  3426  difrab  3438  reupick3  3449  inssdif0im  3519  rexdifpr  3651  rexdifsn  3755  unidif0  4201  bnd2  4207  eqvinop  4277  copsexg  4278  uniuni  4487  rabxp  4701  elvvv  4727  rexiunxp  4809  resopab2  4994  ssrnres  5113  elxp4  5158  elxp5  5159  cnvresima  5160  mptpreima  5164  coass  5189  dff1o2  5512  eqfnfv3  5664  rexsupp  5689  isoini  5868  f1oiso  5876  oprabid  5957  dfoprab2  5973  mpoeq123  5985  mpomptx  6017  resoprab2  6023  ovi3  6064  oprabex3  6195  spc2ed  6300  f1od2  6302  brtpos2  6318  mapsnen  6879  xpsnen  6889  xpcomco  6894  xpassen  6898  ltexpi  7423  enq0enq  7517  enq0tr  7520  prnmaxl  7574  prnminu  7575  genpdflem  7593  ltexprlemm  7686  suplocsrlemb  7892  axaddf  7954  axmulf  7955  rexuz  9673  rexuz2  9674  rexrp  9770  elixx3g  9995  elfz2  10109  fzdifsuc  10175  fzind2  10334  divalgb  12109  gcdass  12209  nnwosdc  12233  lcmass  12280  isprm2  12312  infpn2  12700  fngsum  13092  igsumvalx  13093  issubg3  13400  dfrhm2  13788  ntreq0  14476  tx1cn  14613  tx2cn  14614  blres  14778  metrest  14850  elcncf1di  14923  dedekindicclemicc  14976  fsumdvdsmul  15335  lgsquadlem1  15426  lgsquadlem2  15427