Theorem 3anass 977

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 975	. 2 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ ((𝜑 ∧ 𝜓) ∧ 𝜒))
2		anass 399	. 2 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))
3	1, 2	bitri 183	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

Syntax hints:   ∧ wa 103   ↔ wb 104   ∧ w3a 973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107

This theorem depends on definitions:  df-bi 116  df-3an 975

This theorem is referenced by:  3anrot  978  3anan12  985  anandi3  986  3exdistr  1908  r3al  2514  ceqsex2  2770  ceqsex3v  2772  ceqsex4v  2773  ceqsex6v  2774  ceqsex8v  2775  eldifpr  3610  rexdifpr  3611  trel3  4095  sowlin  4305  dff1o4  5450  mpoxopovel  6220  dfsmo2  6266  ecopovtrn  6610  ecopovtrng  6613  elixp2  6680  elixp  6683  mptelixpg  6712  eqinfti  6997  distrnqg  7349  recmulnqg  7353  ltexnqq  7370  enq0tr  7396  distrnq0  7421  genpdflem  7469  distrlem1prl  7544  distrlem1pru  7545  divmulasscomap  8613  muldivdirap  8624  divmuldivap  8629  prime  9311  eluz2  9493  raluz2  9538  elixx1  9854  elixx3g  9858  elioo2  9878  elioo5  9890  elicc4  9897  iccneg  9946  icoshft  9947  elfz1  9970  elfz  9971  elfz2  9972  elfzm11  10047  elfz2nn0  10068  elfzo2  10106  elfzo3  10119  lbfzo0  10137  fzind2  10195  zmodid2  10308  redivap  10838  imdivap  10845  maxleast  11177  cosmul  11708  dfgcd2  11969  lcmneg  12028  coprmgcdb  12042  divgcdcoprmex  12056  cncongr1  12057  cncongr2  12058  difsqpwdvds  12291  elgz  12323  mgmsscl  12615  ismhm  12685  mhmpropd  12689  issubm  12695  lmbrf  13009  uptx  13068  txcn  13069  xmetec  13231  bl2ioo  13336  lgsmodeq  13740  lgsmulsqcoprm  13741  findset  13980