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:  mpan10  466  an12  551  an32  552  an13  553  an31  554  an4  576  3anass  972  sbidm  1839  4exdistr  1904  2sb5  1971  2sb5rf  1977  sbel2x  1986  r2exf  2484  r19.41  2621  ceqsex3v  2768  ceqsrex2v  2858  rexrab  2889  rexrab2  2893  rexss  3209  inass  3332  difin2  3384  difrab  3396  reupick3  3407  inssdif0im  3476  rexdifpr  3604  rexdifsn  3708  unidif0  4146  bnd2  4152  eqvinop  4221  copsexg  4222  uniuni  4429  rabxp  4641  elvvv  4667  rexiunxp  4746  resopab2  4931  ssrnres  5046  elxp4  5091  elxp5  5092  cnvresima  5093  mptpreima  5097  coass  5122  dff1o2  5437  eqfnfv3  5585  rexsupp  5609  isoini  5786  f1oiso  5794  oprabid  5874  dfoprab2  5889  mpoeq123  5901  mpomptx  5933  resoprab2  5939  ovi3  5978  oprabex3  6097  spc2ed  6201  f1od2  6203  brtpos2  6219  mapsnen  6777  xpsnen  6787  xpcomco  6792  xpassen  6796  ltexpi  7278  enq0enq  7372  enq0tr  7375  prnmaxl  7429  prnminu  7430  genpdflem  7448  ltexprlemm  7541  suplocsrlemb  7747  axaddf  7809  axmulf  7810  rexuz  9518  rexuz2  9519  rexrp  9612  elixx3g  9837  elfz2  9951  fzdifsuc  10016  fzind2  10174  divalgb  11862  gcdass  11948  nnwosdc  11972  lcmass  12017  isprm2  12049  infpn2  12389  ntreq0  12772  tx1cn  12909  tx2cn  12910  blres  13074  metrest  13146  elcncf1di  13206  dedekindicclemicc  13250