Theorem 3anass 985

Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)

Assertion

Ref	Expression
3anass	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Proof of Theorem 3anass

Step	Hyp	Ref	Expression
1		df-3an 983	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 401	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 184	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 981

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  df-3an 983

This theorem is referenced by:  3anrot  986  3anan12  993  anandi3  994  3biant1d  1367  3exdistr  1939  r3al  2550  ceqsex2  2813  ceqsex3v  2815  ceqsex4v  2816  ceqsex6v  2817  ceqsex8v  2818  eldifpr  3660  rexdifpr  3661  trel3  4151  sowlin  4368  dff1o4  5532  mpoxopovel  6329  dfsmo2  6375  ecopovtrn  6721  ecopovtrng  6724  elixp2  6791  elixp  6794  mptelixpg  6823  eqinfti  7124  distrnqg  7502  recmulnqg  7506  ltexnqq  7523  enq0tr  7549  distrnq0  7574  genpdflem  7622  distrlem1prl  7697  distrlem1pru  7698  divmulasscomap  8771  muldivdirap  8782  divmuldivap  8787  prime  9474  eluz2  9656  raluz2  9702  elixx1  10021  elixx3g  10025  elioo2  10045  elioo5  10057  elicc4  10064  iccneg  10113  icoshft  10114  elfz1  10137  elfz  10138  elfz2  10139  elfzm11  10215  elfz2nn0  10236  elfzo2  10274  elfzo3  10288  lbfzo0  10307  fzind2  10370  zmodid2  10499  redivap  11218  imdivap  11225  maxleast  11557  cosmul  12089  bitsval  12287  bitsmod  12300  bitscmp  12302  dfgcd2  12368  lcmneg  12429  coprmgcdb  12443  divgcdcoprmex  12457  cncongr1  12458  cncongr2  12459  difsqpwdvds  12694  elgz  12727  xpsfrnel  13209  xpsfrnel2  13211  mgmsscl  13226  ismhm  13326  mhmpropd  13331  issubm  13337  issubg  13542  eqglact  13594  eqgid  13595  ecqusaddd  13607  ecqusaddcl  13608  isrng  13729  issrg  13760  srglmhm  13788  srgrmhm  13789  isring  13795  ringlghm  13856  dfrhm2  13949  issubrng  13994  issubrg3  14042  islmod  14086  islssm  14152  islssmg  14153  lsspropdg  14226  qusmulrng  14327  lmbrf  14720  uptx  14779  txcn  14780  xmetec  14942  bl2ioo  15055  lgsmodeq  15555  lgsmulsqcoprm  15556  findset  15918