Theorem anass 398

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 397	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		id 19	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	anasss 396	. 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  465  an12  550  an32  551  an13  552  an31  553  an4  575  3anass  966  sbidm  1823  4exdistr  1888  2sb5  1958  2sb5rf  1964  sbel2x  1973  r2exf  2453  r19.41  2586  ceqsex3v  2728  ceqsrex2v  2817  rexrab  2847  rexrab2  2851  rexss  3164  inass  3286  difin2  3338  difrab  3350  reupick3  3361  inssdif0im  3430  rexdifsn  3655  unidif0  4091  bnd2  4097  eqvinop  4165  copsexg  4166  uniuni  4372  rabxp  4576  elvvv  4602  rexiunxp  4681  resopab2  4866  ssrnres  4981  elxp4  5026  elxp5  5027  cnvresima  5028  mptpreima  5032  coass  5057  dff1o2  5372  eqfnfv3  5520  rexsupp  5544  isoini  5719  f1oiso  5727  oprabid  5803  dfoprab2  5818  mpoeq123  5830  mpomptx  5862  resoprab2  5868  ovi3  5907  oprabex3  6027  spc2ed  6130  f1od2  6132  brtpos2  6148  mapsnen  6705  xpsnen  6715  xpcomco  6720  xpassen  6724  ltexpi  7145  enq0enq  7239  enq0tr  7242  prnmaxl  7296  prnminu  7297  genpdflem  7315  ltexprlemm  7408  suplocsrlemb  7614  axaddf  7676  axmulf  7677  rexuz  9375  rexuz2  9376  rexrp  9464  elixx3g  9684  elfz2  9797  fzdifsuc  9861  fzind2  10016  divalgb  11622  gcdass  11703  lcmass  11766  isprm2  11798  ntreq0  12301  tx1cn  12438  tx2cn  12439  blres  12603  metrest  12675  elcncf1di  12735  dedekindicclemicc  12779