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  982  sbidm  1851  4exdistr  1916  2sb5  1983  2sb5rf  1989  sbel2x  1998  r2exf  2495  r19.41  2632  ceqsex3v  2779  ceqsrex2v  2869  rexrab  2900  rexrab2  2904  rexss  3222  inass  3345  difin2  3397  difrab  3409  reupick3  3420  inssdif0im  3490  rexdifpr  3620  rexdifsn  3724  unidif0  4167  bnd2  4173  eqvinop  4243  copsexg  4244  uniuni  4451  rabxp  4663  elvvv  4689  rexiunxp  4769  resopab2  4954  ssrnres  5071  elxp4  5116  elxp5  5117  cnvresima  5118  mptpreima  5122  coass  5147  dff1o2  5466  eqfnfv3  5615  rexsupp  5640  isoini  5818  f1oiso  5826  oprabid  5906  dfoprab2  5921  mpoeq123  5933  mpomptx  5965  resoprab2  5971  ovi3  6010  oprabex3  6129  spc2ed  6233  f1od2  6235  brtpos2  6251  mapsnen  6810  xpsnen  6820  xpcomco  6825  xpassen  6829  ltexpi  7335  enq0enq  7429  enq0tr  7432  prnmaxl  7486  prnminu  7487  genpdflem  7505  ltexprlemm  7598  suplocsrlemb  7804  axaddf  7866  axmulf  7867  rexuz  9579  rexuz2  9580  rexrp  9675  elixx3g  9900  elfz2  10014  fzdifsuc  10080  fzind2  10238  divalgb  11929  gcdass  12015  nnwosdc  12039  lcmass  12084  isprm2  12116  infpn2  12456  issubg3  13050  ntreq0  13602  tx1cn  13739  tx2cn  13740  blres  13904  metrest  13976  elcncf1di  14036  dedekindicclemicc  14080