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 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used 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  inssdif0imOLD  3593  rexdifpr  3737  rexdifsn  3846  unidif0  4306  bnd2  4312  eqvinop  4385  copsexg  4386  uniuni  4599  rabxp  4814  elvvv  4840  rexiunxp  4924  resopab2  5113  ssrnres  5233  elxp4  5278  elxp5  5279  cnvresima  5280  mptpreima  5284  coass  5309  dff1o2  5647  eqfnfv3  5811  isoini  6027  f1oiso  6035  oprabid  6120  dfoprab2  6138  mpoeq123  6150  mpomptx  6182  resoprab2  6188  ovi3  6229  oprabex3  6366  spc2ed  6473  f1od2  6475  rexsupp  6497  brtpos2  6526  mapsnend  7103  mapsnen  7104  xpsnen  7123  xpcomco  7128  xpassen  7132  ltexpi  7710  enq0enq  7804  enq0tr  7807  prnmaxl  7861  prnminu  7862  genpdflem  7880  ltexprlemm  7973  suplocsrlemb  8179  axaddf  8241  axmulf  8242  rexuz  9996  rexuz2  9997  rexrp  10094  elixx3g  10320  elfz2  10435  fzdifsuc  10505  fzind2  10675  sseqn  11301  hashfibclem  11304  divalgb  12717  gcdass  12817  nnwosdc  12841  lcmass  12888  isprm2  12920  infpn2  13405  fngzsum  13767  gzsumvalx  13768  issubg3  14054  resscntz  14166  dfrhm2  14570  ntreq0  15358  tx1cn  15495  tx2cn  15496  blres  15660  metrest  15732  elcncf1di  15805  dedekindicclemicc  15858  fsumdvdsmul  16285  lgsquadlem1  16401  lgsquadlem2  16402  wlk1walkdom  16805  isclwwlk  16840  isclwwlknx  16862  clwwlknonel  16878  clwwlknon2x  16881  iseupthf1o  16894  idjudju  17252  alsanmo  17358  ralsanmo  17359  2alsraln0m  17365