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  2844  ceqsrex2v  2936  rexrab  2967  rexrab2  2971  rexss  3292  inass  3415  difin2  3467  difrab  3479  reupick3  3490  inssdif0im  3560  rexdifpr  3695  rexdifsn  3803  unidif0  4255  bnd2  4261  eqvinop  4333  copsexg  4334  uniuni  4546  rabxp  4761  elvvv  4787  rexiunxp  4870  resopab2  5058  ssrnres  5177  elxp4  5222  elxp5  5223  cnvresima  5224  mptpreima  5228  coass  5253  dff1o2  5585  eqfnfv3  5742  rexsupp  5767  isoini  5954  f1oiso  5962  oprabid  6045  dfoprab2  6063  mpoeq123  6075  mpomptx  6107  resoprab2  6113  ovi3  6154  oprabex3  6286  spc2ed  6393  f1od2  6395  brtpos2  6412  mapsnen  6981  xpsnen  7000  xpcomco  7005  xpassen  7009  ltexpi  7547  enq0enq  7641  enq0tr  7644  prnmaxl  7698  prnminu  7699  genpdflem  7717  ltexprlemm  7810  suplocsrlemb  8016  axaddf  8078  axmulf  8079  rexuz  9804  rexuz2  9805  rexrp  9901  elixx3g  10126  elfz2  10240  fzdifsuc  10306  fzind2  10475  divalgb  12476  gcdass  12576  nnwosdc  12600  lcmass  12647  isprm2  12679  infpn2  13067  fngsum  13461  igsumvalx  13462  issubg3  13769  dfrhm2  14158  ntreq0  14846  tx1cn  14983  tx2cn  14984  blres  15148  metrest  15220  elcncf1di  15293  dedekindicclemicc  15346  fsumdvdsmul  15705  lgsquadlem1  15796  lgsquadlem2  15797  wlk1walkdom  16156  isclwwlk  16189  isclwwlknx  16211  clwwlknonel  16227  clwwlknon2x  16230  iseupthf1o  16243