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  1006  sbidm  1897  4exdistr  1963  2sb5  2034  2sb5rf  2040  sbel2x  2049  r2exf  2548  r19.41  2686  ceqsex3v  2843  ceqsrex2v  2935  rexrab  2966  rexrab2  2970  rexss  3291  inass  3414  difin2  3466  difrab  3478  reupick3  3489  inssdif0im  3559  rexdifpr  3694  rexdifsn  3800  unidif0  4251  bnd2  4257  eqvinop  4329  copsexg  4330  uniuni  4542  rabxp  4756  elvvv  4782  rexiunxp  4864  resopab2  5052  ssrnres  5171  elxp4  5216  elxp5  5217  cnvresima  5218  mptpreima  5222  coass  5247  dff1o2  5579  eqfnfv3  5736  rexsupp  5761  isoini  5948  f1oiso  5956  oprabid  6039  dfoprab2  6057  mpoeq123  6069  mpomptx  6101  resoprab2  6107  ovi3  6148  oprabex3  6280  spc2ed  6385  f1od2  6387  brtpos2  6403  mapsnen  6972  xpsnen  6988  xpcomco  6993  xpassen  6997  ltexpi  7535  enq0enq  7629  enq0tr  7632  prnmaxl  7686  prnminu  7687  genpdflem  7705  ltexprlemm  7798  suplocsrlemb  8004  axaddf  8066  axmulf  8067  rexuz  9787  rexuz2  9788  rexrp  9884  elixx3g  10109  elfz2  10223  fzdifsuc  10289  fzind2  10457  divalgb  12452  gcdass  12552  nnwosdc  12576  lcmass  12623  isprm2  12655  infpn2  13043  fngsum  13437  igsumvalx  13438  issubg3  13745  dfrhm2  14134  ntreq0  14822  tx1cn  14959  tx2cn  14960  blres  15124  metrest  15196  elcncf1di  15269  dedekindicclemicc  15322  fsumdvdsmul  15681  lgsquadlem1  15772  lgsquadlem2  15773  wlk1walkdom  16105  isclwwlk  16137  isclwwlknx  16158