Theorem anass 399

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 398	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		id 19	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	anasss 397	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
5	2, 4	impbii 125	1 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ∧ wa 103   ↔ wb 104

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

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  bianass  466  mpan10  471  an12  556  an32  557  an13  558  an31  559  an4  581  3anass  977  sbidm  1844  4exdistr  1909  2sb5  1976  2sb5rf  1982  sbel2x  1991  r2exf  2488  r19.41  2625  ceqsex3v  2772  ceqsrex2v  2862  rexrab  2893  rexrab2  2897  rexss  3214  inass  3337  difin2  3389  difrab  3401  reupick3  3412  inssdif0im  3481  rexdifpr  3609  rexdifsn  3713  unidif0  4151  bnd2  4157  eqvinop  4226  copsexg  4227  uniuni  4434  rabxp  4646  elvvv  4672  rexiunxp  4751  resopab2  4936  ssrnres  5051  elxp4  5096  elxp5  5097  cnvresima  5098  mptpreima  5102  coass  5127  dff1o2  5445  eqfnfv3  5593  rexsupp  5617  isoini  5794  f1oiso  5802  oprabid  5882  dfoprab2  5897  mpoeq123  5909  mpomptx  5941  resoprab2  5947  ovi3  5986  oprabex3  6105  spc2ed  6209  f1od2  6211  brtpos2  6227  mapsnen  6785  xpsnen  6795  xpcomco  6800  xpassen  6804  ltexpi  7286  enq0enq  7380  enq0tr  7383  prnmaxl  7437  prnminu  7438  genpdflem  7456  ltexprlemm  7549  suplocsrlemb  7755  axaddf  7817  axmulf  7818  rexuz  9526  rexuz2  9527  rexrp  9620  elixx3g  9845  elfz2  9959  fzdifsuc  10024  fzind2  10182  divalgb  11871  gcdass  11957  nnwosdc  11981  lcmass  12026  isprm2  12058  infpn2  12398  ntreq0  12847  tx1cn  12984  tx2cn  12985  blres  13149  metrest  13221  elcncf1di  13281  dedekindicclemicc  13325