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  985  sbidm  1875  4exdistr  1941  2sb5  2012  2sb5rf  2018  sbel2x  2027  r2exf  2526  r19.41  2663  ceqsex3v  2820  ceqsrex2v  2912  rexrab  2943  rexrab2  2947  rexss  3268  inass  3391  difin2  3443  difrab  3455  reupick3  3466  inssdif0im  3536  rexdifpr  3671  rexdifsn  3776  unidif0  4227  bnd2  4233  eqvinop  4305  copsexg  4306  uniuni  4516  rabxp  4730  elvvv  4756  rexiunxp  4838  resopab2  5025  ssrnres  5144  elxp4  5189  elxp5  5190  cnvresima  5191  mptpreima  5195  coass  5220  dff1o2  5549  eqfnfv3  5702  rexsupp  5727  isoini  5910  f1oiso  5918  oprabid  5999  dfoprab2  6015  mpoeq123  6027  mpomptx  6059  resoprab2  6065  ovi3  6106  oprabex3  6237  spc2ed  6342  f1od2  6344  brtpos2  6360  mapsnen  6927  xpsnen  6941  xpcomco  6946  xpassen  6950  ltexpi  7485  enq0enq  7579  enq0tr  7582  prnmaxl  7636  prnminu  7637  genpdflem  7655  ltexprlemm  7748  suplocsrlemb  7954  axaddf  8016  axmulf  8017  rexuz  9736  rexuz2  9737  rexrp  9833  elixx3g  10058  elfz2  10172  fzdifsuc  10238  fzind2  10405  divalgb  12351  gcdass  12451  nnwosdc  12475  lcmass  12522  isprm2  12554  infpn2  12942  fngsum  13335  igsumvalx  13336  issubg3  13643  dfrhm2  14031  ntreq0  14719  tx1cn  14856  tx2cn  14857  blres  15021  metrest  15093  elcncf1di  15166  dedekindicclemicc  15219  fsumdvdsmul  15578  lgsquadlem1  15669  lgsquadlem2  15670