Theorem 3anass 972

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

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

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 970

This theorem is referenced by:  3anrot  973  3anan12  980  anandi3  981  3exdistr  1903  r3al  2510  ceqsex2  2766  ceqsex3v  2768  ceqsex4v  2769  ceqsex6v  2770  ceqsex8v  2771  eldifpr  3603  rexdifpr  3604  trel3  4088  sowlin  4298  dff1o4  5440  mpoxopovel  6209  dfsmo2  6255  ecopovtrn  6598  ecopovtrng  6601  elixp2  6668  elixp  6671  mptelixpg  6700  eqinfti  6985  distrnqg  7328  recmulnqg  7332  ltexnqq  7349  enq0tr  7375  distrnq0  7400  genpdflem  7448  distrlem1prl  7523  distrlem1pru  7524  divmulasscomap  8592  muldivdirap  8603  divmuldivap  8608  prime  9290  eluz2  9472  raluz2  9517  elixx1  9833  elixx3g  9837  elioo2  9857  elioo5  9869  elicc4  9876  iccneg  9925  icoshft  9926  elfz1  9949  elfz  9950  elfz2  9951  elfzm11  10026  elfz2nn0  10047  elfzo2  10085  elfzo3  10098  lbfzo0  10116  fzind2  10174  zmodid2  10287  redivap  10816  imdivap  10823  maxleast  11155  cosmul  11686  dfgcd2  11947  lcmneg  12006  coprmgcdb  12020  divgcdcoprmex  12034  cncongr1  12035  cncongr2  12036  difsqpwdvds  12269  elgz  12301  mgmsscl  12592  lmbrf  12855  uptx  12914  txcn  12915  xmetec  13077  bl2ioo  13182  lgsmodeq  13586  lgsmulsqcoprm  13587  findset  13827