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  984  sbidm  1873  4exdistr  1939  2sb5  2010  2sb5rf  2016  sbel2x  2025  r2exf  2523  r19.41  2660  ceqsex3v  2814  ceqsrex2v  2904  rexrab  2935  rexrab2  2939  rexss  3259  inass  3382  difin2  3434  difrab  3446  reupick3  3457  inssdif0im  3527  rexdifpr  3660  rexdifsn  3764  unidif0  4210  bnd2  4216  eqvinop  4286  copsexg  4287  uniuni  4497  rabxp  4711  elvvv  4737  rexiunxp  4819  resopab2  5005  ssrnres  5124  elxp4  5169  elxp5  5170  cnvresima  5171  mptpreima  5175  coass  5200  dff1o2  5526  eqfnfv3  5678  rexsupp  5703  isoini  5886  f1oiso  5894  oprabid  5975  dfoprab2  5991  mpoeq123  6003  mpomptx  6035  resoprab2  6041  ovi3  6082  oprabex3  6213  spc2ed  6318  f1od2  6320  brtpos2  6336  mapsnen  6902  xpsnen  6915  xpcomco  6920  xpassen  6924  ltexpi  7449  enq0enq  7543  enq0tr  7546  prnmaxl  7600  prnminu  7601  genpdflem  7619  ltexprlemm  7712  suplocsrlemb  7918  axaddf  7980  axmulf  7981  rexuz  9700  rexuz2  9701  rexrp  9797  elixx3g  10022  elfz2  10136  fzdifsuc  10202  fzind2  10366  divalgb  12207  gcdass  12307  nnwosdc  12331  lcmass  12378  isprm2  12410  infpn2  12798  fngsum  13191  igsumvalx  13192  issubg3  13499  dfrhm2  13887  ntreq0  14575  tx1cn  14712  tx2cn  14713  blres  14877  metrest  14949  elcncf1di  15022  dedekindicclemicc  15075  fsumdvdsmul  15434  lgsquadlem1  15525  lgsquadlem2  15526