Theorem anass 405

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 404	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → (𝜑 ∧ (𝜓 ∧ 𝜒)))
3		id 19	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → ((𝜑 ∧ 𝜓) ∧ 𝜒))
4	3	anasss 403	. 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  473  mpan10  478  an12  567  an32  568  an13  569  an31  570  an4  592  3anass  1013  sbidm  1904  4exdistr  1972  2sb5  2043  2sb5rf  2049  sbel2x  2058  r2exf  2568  r19.41  2706  ceqsex3v  2865  ceqsrex2v  2958  rexrab  2989  rexrab2  2993  rexss  3315  inass  3441  difin2  3493  difrab  3507  reupick3  3518  inssdif0im  3591  rexdifpr  3733  rexdifsn  3841  unidif0  4299  bnd2  4305  eqvinop  4378  copsexg  4379  uniuni  4592  rabxp  4807  elvvv  4833  rexiunxp  4917  resopab2  5105  ssrnres  5225  elxp4  5270  elxp5  5271  cnvresima  5272  mptpreima  5276  coass  5301  dff1o2  5639  eqfnfv3  5799  isoini  6014  f1oiso  6022  oprabid  6107  dfoprab2  6125  mpoeq123  6137  mpomptx  6169  resoprab2  6175  ovi3  6216  oprabex3  6352  spc2ed  6459  f1od2  6461  rexsupp  6483  brtpos2  6512  mapsnend  7089  mapsnen  7090  xpsnen  7109  xpcomco  7114  xpassen  7118  ltexpi  7694  enq0enq  7788  enq0tr  7791  prnmaxl  7845  prnminu  7846  genpdflem  7864  ltexprlemm  7957  suplocsrlemb  8163  axaddf  8225  axmulf  8226  rexuz  9959  rexuz2  9960  rexrp  10056  elixx3g  10282  elfz2  10397  fzdifsuc  10466  fzind2  10636  sseqn  11257  hashfibclem  11260  divalgb  12670  gcdass  12770  nnwosdc  12794  lcmass  12841  isprm2  12873  infpn2  13325  fngzsum  13685  gzsumvalx  13686  issubg3  13972  dfrhm2  14434  ntreq0  15156  tx1cn  15293  tx2cn  15294  blres  15458  metrest  15530  elcncf1di  15603  dedekindicclemicc  15656  fsumdvdsmul  16019  lgsquadlem1  16110  lgsquadlem2  16111  wlk1walkdom  16514  isclwwlk  16549  isclwwlknx  16571  clwwlknonel  16587  clwwlknon2x  16590  iseupthf1o  16603