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  5959  f1oiso  5967  oprabid  6050  dfoprab2  6068  mpoeq123  6080  mpomptx  6112  resoprab2  6118  ovi3  6159  oprabex3  6291  spc2ed  6398  f1od2  6400  brtpos2  6417  mapsnen  6986  xpsnen  7005  xpcomco  7010  xpassen  7014  ltexpi  7557  enq0enq  7651  enq0tr  7654  prnmaxl  7708  prnminu  7709  genpdflem  7727  ltexprlemm  7820  suplocsrlemb  8026  axaddf  8088  axmulf  8089  rexuz  9814  rexuz2  9815  rexrp  9911  elixx3g  10136  elfz2  10250  fzdifsuc  10316  fzind2  10486  divalgb  12504  gcdass  12604  nnwosdc  12628  lcmass  12675  isprm2  12707  infpn2  13095  fngsum  13489  igsumvalx  13490  issubg3  13797  dfrhm2  14187  ntreq0  14875  tx1cn  15012  tx2cn  15013  blres  15177  metrest  15249  elcncf1di  15322  dedekindicclemicc  15375  fsumdvdsmul  15734  lgsquadlem1  15825  lgsquadlem2  15826  wlk1walkdom  16229  isclwwlk  16264  isclwwlknx  16286  clwwlknonel  16302  clwwlknon2x  16305  iseupthf1o  16318