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  563  an32  564  an13  565  an31  566  an4  588  3anass  1008  sbidm  1899  4exdistr  1965  2sb5  2036  2sb5rf  2042  sbel2x  2051  r2exf  2550  r19.41  2688  ceqsex3v  2846  ceqsrex2v  2938  rexrab  2969  rexrab2  2973  rexss  3294  inass  3417  difin2  3469  difrab  3481  reupick3  3492  inssdif0im  3562  rexdifpr  3697  rexdifsn  3805  unidif0  4257  bnd2  4263  eqvinop  4335  copsexg  4336  uniuni  4548  rabxp  4763  elvvv  4789  rexiunxp  4872  resopab2  5060  ssrnres  5179  elxp4  5224  elxp5  5225  cnvresima  5226  mptpreima  5230  coass  5255  dff1o2  5588  eqfnfv3  5746  rexsupp  5771  isoini  5958  f1oiso  5966  oprabid  6049  dfoprab2  6067  mpoeq123  6079  mpomptx  6111  resoprab2  6117  ovi3  6158  oprabex3  6290  spc2ed  6397  f1od2  6399  brtpos2  6416  mapsnen  6985  xpsnen  7004  xpcomco  7009  xpassen  7013  ltexpi  7556  enq0enq  7650  enq0tr  7653  prnmaxl  7707  prnminu  7708  genpdflem  7726  ltexprlemm  7819  suplocsrlemb  8025  axaddf  8087  axmulf  8088  rexuz  9813  rexuz2  9814  rexrp  9910  elixx3g  10135  elfz2  10249  fzdifsuc  10315  fzind2  10484  divalgb  12485  gcdass  12585  nnwosdc  12609  lcmass  12656  isprm2  12688  infpn2  13076  fngsum  13470  igsumvalx  13471  issubg3  13778  dfrhm2  14167  ntreq0  14855  tx1cn  14992  tx2cn  14993  blres  15157  metrest  15229  elcncf1di  15302  dedekindicclemicc  15355  fsumdvdsmul  15714  lgsquadlem1  15805  lgsquadlem2  15806  wlk1walkdom  16209  isclwwlk  16244  isclwwlknx  16266  clwwlknonel  16282  clwwlknon2x  16285  iseupthf1o  16298