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  561  an32  562  an13  563  an31  564  an4  586  3anass  1006  sbidm  1897  4exdistr  1963  2sb5  2034  2sb5rf  2040  sbel2x  2049  r2exf  2548  r19.41  2686  ceqsex3v  2843  ceqsrex2v  2935  rexrab  2966  rexrab2  2970  rexss  3291  inass  3414  difin2  3466  difrab  3478  reupick3  3489  inssdif0im  3559  rexdifpr  3694  rexdifsn  3800  unidif0  4251  bnd2  4257  eqvinop  4329  copsexg  4330  uniuni  4542  rabxp  4756  elvvv  4782  rexiunxp  4864  resopab2  5052  ssrnres  5171  elxp4  5216  elxp5  5217  cnvresima  5218  mptpreima  5222  coass  5247  dff1o2  5577  eqfnfv3  5734  rexsupp  5759  isoini  5942  f1oiso  5950  oprabid  6033  dfoprab2  6051  mpoeq123  6063  mpomptx  6095  resoprab2  6101  ovi3  6142  oprabex3  6274  spc2ed  6379  f1od2  6381  brtpos2  6397  mapsnen  6964  xpsnen  6980  xpcomco  6985  xpassen  6989  ltexpi  7524  enq0enq  7618  enq0tr  7621  prnmaxl  7675  prnminu  7676  genpdflem  7694  ltexprlemm  7787  suplocsrlemb  7993  axaddf  8055  axmulf  8056  rexuz  9775  rexuz2  9776  rexrp  9872  elixx3g  10097  elfz2  10211  fzdifsuc  10277  fzind2  10445  divalgb  12436  gcdass  12536  nnwosdc  12560  lcmass  12607  isprm2  12639  infpn2  13027  fngsum  13421  igsumvalx  13422  issubg3  13729  dfrhm2  14118  ntreq0  14806  tx1cn  14943  tx2cn  14944  blres  15108  metrest  15180  elcncf1di  15253  dedekindicclemicc  15306  fsumdvdsmul  15665  lgsquadlem1  15756  lgsquadlem2  15757  wlk1walkdom  16070