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  1862  4exdistr  1928  2sb5  1999  2sb5rf  2005  sbel2x  2014  r2exf  2512  r19.41  2649  ceqsex3v  2803  ceqsrex2v  2893  rexrab  2924  rexrab2  2928  rexss  3247  inass  3370  difin2  3422  difrab  3434  reupick3  3445  inssdif0im  3515  rexdifpr  3647  rexdifsn  3751  unidif0  4197  bnd2  4203  eqvinop  4273  copsexg  4274  uniuni  4483  rabxp  4697  elvvv  4723  rexiunxp  4805  resopab2  4990  ssrnres  5109  elxp4  5154  elxp5  5155  cnvresima  5156  mptpreima  5160  coass  5185  dff1o2  5506  eqfnfv3  5658  rexsupp  5683  isoini  5862  f1oiso  5870  oprabid  5951  dfoprab2  5966  mpoeq123  5978  mpomptx  6010  resoprab2  6016  ovi3  6057  oprabex3  6183  spc2ed  6288  f1od2  6290  brtpos2  6306  mapsnen  6867  xpsnen  6877  xpcomco  6882  xpassen  6886  ltexpi  7399  enq0enq  7493  enq0tr  7496  prnmaxl  7550  prnminu  7551  genpdflem  7569  ltexprlemm  7662  suplocsrlemb  7868  axaddf  7930  axmulf  7931  rexuz  9648  rexuz2  9649  rexrp  9745  elixx3g  9970  elfz2  10084  fzdifsuc  10150  fzind2  10309  divalgb  12069  gcdass  12155  nnwosdc  12179  lcmass  12226  isprm2  12258  infpn2  12616  fngsum  12974  igsumvalx  12975  issubg3  13265  dfrhm2  13653  ntreq0  14311  tx1cn  14448  tx2cn  14449  blres  14613  metrest  14685  elcncf1di  14758  dedekindicclemicc  14811  lgsquadlem1  15234  lgsquadlem2  15235