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  1009  sbidm  1900  4exdistr  1966  2sb5  2037  2sb5rf  2043  sbel2x  2052  r2exf  2560  r19.41  2698  ceqsex3v  2857  ceqsrex2v  2949  rexrab  2980  rexrab2  2984  rexss  3305  inass  3431  difin2  3483  difrab  3495  reupick3  3506  inssdif0im  3576  rexdifpr  3717  rexdifsn  3825  unidif0  4280  bnd2  4286  eqvinop  4359  copsexg  4360  uniuni  4572  rabxp  4787  elvvv  4813  rexiunxp  4897  resopab2  5085  ssrnres  5205  elxp4  5250  elxp5  5251  cnvresima  5252  mptpreima  5256  coass  5281  dff1o2  5619  eqfnfv3  5777  isoini  5991  f1oiso  5999  oprabid  6082  dfoprab2  6100  mpoeq123  6112  mpomptx  6144  resoprab2  6150  ovi3  6191  oprabex3  6322  spc2ed  6429  f1od2  6431  rexsupp  6453  brtpos2  6482  mapsnend  7052  mapsnen  7053  xpsnen  7072  xpcomco  7077  xpassen  7081  ltexpi  7652  enq0enq  7746  enq0tr  7749  prnmaxl  7803  prnminu  7804  genpdflem  7822  ltexprlemm  7915  suplocsrlemb  8121  axaddf  8183  axmulf  8184  rexuz  9912  rexuz2  9913  rexrp  10009  elixx3g  10234  elfz2  10349  fzdifsuc  10415  fzind2  10585  sseqn  11203  hashfibclem  11206  divalgb  12611  gcdass  12711  nnwosdc  12735  lcmass  12782  isprm2  12814  infpn2  13207  fngsum  13601  igsumvalx  13602  issubg3  13909  dfrhm2  14299  ntreq0  14997  tx1cn  15134  tx2cn  15135  blres  15299  metrest  15371  elcncf1di  15444  dedekindicclemicc  15497  fsumdvdsmul  15859  lgsquadlem1  15950  lgsquadlem2  15951  wlk1walkdom  16354  isclwwlk  16389  isclwwlknx  16411  clwwlknonel  16427  clwwlknon2x  16430  iseupthf1o  16443