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  985  sbidm  1874  4exdistr  1940  2sb5  2011  2sb5rf  2017  sbel2x  2026  r2exf  2524  r19.41  2661  ceqsex3v  2815  ceqsrex2v  2905  rexrab  2936  rexrab2  2940  rexss  3260  inass  3383  difin2  3435  difrab  3447  reupick3  3458  inssdif0im  3528  rexdifpr  3661  rexdifsn  3765  unidif0  4211  bnd2  4217  eqvinop  4287  copsexg  4288  uniuni  4498  rabxp  4712  elvvv  4738  rexiunxp  4820  resopab2  5006  ssrnres  5125  elxp4  5170  elxp5  5171  cnvresima  5172  mptpreima  5176  coass  5201  dff1o2  5527  eqfnfv3  5679  rexsupp  5704  isoini  5887  f1oiso  5895  oprabid  5976  dfoprab2  5992  mpoeq123  6004  mpomptx  6036  resoprab2  6042  ovi3  6083  oprabex3  6214  spc2ed  6319  f1od2  6321  brtpos2  6337  mapsnen  6903  xpsnen  6916  xpcomco  6921  xpassen  6925  ltexpi  7450  enq0enq  7544  enq0tr  7547  prnmaxl  7601  prnminu  7602  genpdflem  7620  ltexprlemm  7713  suplocsrlemb  7919  axaddf  7981  axmulf  7982  rexuz  9701  rexuz2  9702  rexrp  9798  elixx3g  10023  elfz2  10137  fzdifsuc  10203  fzind2  10368  divalgb  12236  gcdass  12336  nnwosdc  12360  lcmass  12407  isprm2  12439  infpn2  12827  fngsum  13220  igsumvalx  13221  issubg3  13528  dfrhm2  13916  ntreq0  14604  tx1cn  14741  tx2cn  14742  blres  14906  metrest  14978  elcncf1di  15051  dedekindicclemicc  15104  fsumdvdsmul  15463  lgsquadlem1  15554  lgsquadlem2  15555