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  563  an32  564  an13  565  an31  566  an4  588  3anass  1009  sbidm  1900  4exdistr  1968  2sb5  2039  2sb5rf  2045  sbel2x  2054  r2exf  2562  r19.41  2700  ceqsex3v  2859  ceqsrex2v  2952  rexrab  2983  rexrab2  2987  rexss  3309  inass  3435  difin2  3487  difrab  3499  reupick3  3510  inssdif0im  3580  rexdifpr  3722  rexdifsn  3830  unidif0  4285  bnd2  4291  eqvinop  4364  copsexg  4365  uniuni  4577  rabxp  4792  elvvv  4818  rexiunxp  4902  resopab2  5090  ssrnres  5210  elxp4  5255  elxp5  5256  cnvresima  5257  mptpreima  5261  coass  5286  dff1o2  5624  eqfnfv3  5782  isoini  5997  f1oiso  6005  oprabid  6090  dfoprab2  6108  mpoeq123  6120  mpomptx  6152  resoprab2  6158  ovi3  6199  oprabex3  6335  spc2ed  6442  f1od2  6444  rexsupp  6466  brtpos2  6495  mapsnend  7065  mapsnen  7066  xpsnen  7085  xpcomco  7090  xpassen  7094  ltexpi  7668  enq0enq  7762  enq0tr  7765  prnmaxl  7819  prnminu  7820  genpdflem  7838  ltexprlemm  7931  suplocsrlemb  8137  axaddf  8199  axmulf  8200  rexuz  9930  rexuz2  9931  rexrp  10027  elixx3g  10253  elfz2  10368  fzdifsuc  10437  fzind2  10607  sseqn  11228  hashfibclem  11231  divalgb  12636  gcdass  12736  nnwosdc  12760  lcmass  12807  isprm2  12839  infpn2  13291  fngsum  13651  igsumvalx  13652  issubg3  13945  dfrhm2  14399  ntreq0  15123  tx1cn  15260  tx2cn  15261  blres  15425  metrest  15497  elcncf1di  15570  dedekindicclemicc  15623  fsumdvdsmul  15985  lgsquadlem1  16076  lgsquadlem2  16077  wlk1walkdom  16480  isclwwlk  16515  isclwwlknx  16537  clwwlknonel  16553  clwwlknon2x  16556  iseupthf1o  16569