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  1875  4exdistr  1941  2sb5  2012  2sb5rf  2018  sbel2x  2027  r2exf  2525  r19.41  2662  ceqsex3v  2817  ceqsrex2v  2909  rexrab  2940  rexrab2  2944  rexss  3264  inass  3387  difin2  3439  difrab  3451  reupick3  3462  inssdif0im  3532  rexdifpr  3666  rexdifsn  3771  unidif0  4222  bnd2  4228  eqvinop  4300  copsexg  4301  uniuni  4511  rabxp  4725  elvvv  4751  rexiunxp  4833  resopab2  5020  ssrnres  5139  elxp4  5184  elxp5  5185  cnvresima  5186  mptpreima  5190  coass  5215  dff1o2  5544  eqfnfv3  5697  rexsupp  5722  isoini  5905  f1oiso  5913  oprabid  5994  dfoprab2  6010  mpoeq123  6022  mpomptx  6054  resoprab2  6060  ovi3  6101  oprabex3  6232  spc2ed  6337  f1od2  6339  brtpos2  6355  mapsnen  6922  xpsnen  6936  xpcomco  6941  xpassen  6945  ltexpi  7480  enq0enq  7574  enq0tr  7577  prnmaxl  7631  prnminu  7632  genpdflem  7650  ltexprlemm  7743  suplocsrlemb  7949  axaddf  8011  axmulf  8012  rexuz  9731  rexuz2  9732  rexrp  9828  elixx3g  10053  elfz2  10167  fzdifsuc  10233  fzind2  10400  divalgb  12321  gcdass  12421  nnwosdc  12445  lcmass  12492  isprm2  12524  infpn2  12912  fngsum  13305  igsumvalx  13306  issubg3  13613  dfrhm2  14001  ntreq0  14689  tx1cn  14826  tx2cn  14827  blres  14991  metrest  15063  elcncf1di  15136  dedekindicclemicc  15189  fsumdvdsmul  15548  lgsquadlem1  15639  lgsquadlem2  15640