Theorem 3anass 982

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 980	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 401	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 184	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

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

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 980

This theorem is referenced by:  3anrot  983  3anan12  990  anandi3  991  3exdistr  1915  r3al  2521  ceqsex2  2777  ceqsex3v  2779  ceqsex4v  2780  ceqsex6v  2781  ceqsex8v  2782  eldifpr  3619  rexdifpr  3620  trel3  4109  sowlin  4320  dff1o4  5469  mpoxopovel  6241  dfsmo2  6287  ecopovtrn  6631  ecopovtrng  6634  elixp2  6701  elixp  6704  mptelixpg  6733  eqinfti  7018  distrnqg  7385  recmulnqg  7389  ltexnqq  7406  enq0tr  7432  distrnq0  7457  genpdflem  7505  distrlem1prl  7580  distrlem1pru  7581  divmulasscomap  8652  muldivdirap  8663  divmuldivap  8668  prime  9351  eluz2  9533  raluz2  9578  elixx1  9896  elixx3g  9900  elioo2  9920  elioo5  9932  elicc4  9939  iccneg  9988  icoshft  9989  elfz1  10012  elfz  10013  elfz2  10014  elfzm11  10090  elfz2nn0  10111  elfzo2  10149  elfzo3  10162  lbfzo0  10180  fzind2  10238  zmodid2  10351  redivap  10882  imdivap  10889  maxleast  11221  cosmul  11752  dfgcd2  12014  lcmneg  12073  coprmgcdb  12087  divgcdcoprmex  12101  cncongr1  12102  cncongr2  12103  difsqpwdvds  12336  elgz  12368  xpsfrnel  12762  xpsfrnel2  12764  mgmsscl  12779  ismhm  12852  mhmpropd  12856  issubm  12862  issubg  13031  eqglact  13082  eqgid  13083  issrg  13146  srglmhm  13174  srgrmhm  13175  isring  13181  issubrg3  13366  islmod  13379  lmbrf  13685  uptx  13744  txcn  13745  xmetec  13907  bl2ioo  14012  lgsmodeq  14416  lgsmulsqcoprm  14417  findset  14667