Theorem 3anass 1013

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

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anrot  1014  3anan12  1021  anandi3  1022  3biant1d  1396  3exdistr  1971  r3al  2594  ceqsex2  2863  ceqsex3v  2865  ceqsex4v  2866  ceqsex6v  2867  ceqsex8v  2868  eldifpr  3736  rexdifpr  3737  trel3  4237  sowlin  4465  dff1o4  5647  mpoxopovel  6512  dfsmo2  6558  ecopovtrn  6906  ecopovtrng  6909  elixp2  6984  elixp  6987  mptelixpg  7016  eqinfti  7360  distrnqg  7754  recmulnqg  7758  ltexnqq  7775  enq0tr  7801  distrnq0  7826  genpdflem  7874  distrlem1prl  7949  distrlem1pru  7950  divmulasscomap  9026  muldivdirap  9037  divmuldivap  9042  prime  9745  eluz2  9927  raluz2  9979  elixx1  10299  elixx3g  10303  elioo2  10323  elioo5  10335  elicc4  10342  iccneg  10391  icoshft  10392  elfz1  10416  elfz  10417  elfz2  10418  elfzm11  10498  elfz2nn0  10519  elfzo2  10557  elfzo3  10571  lbfzo0  10592  fzind2  10658  zmodid2  10789  swrdccatin1  11497  swrdccat  11507  redivap  11639  imdivap  11646  maxleast  11979  cosmul  12512  bitsval  12710  bitsmod  12723  bitscmp  12725  dfgcd2  12791  lcmneg  12852  coprmgcdb  12866  divgcdcoprmex  12880  cncongr1  12881  cncongr2  12882  difsqpwdvds  13117  elgz  13150  xpsfrnel  13665  xpsfrnel2  13667  mgmsscl  13681  ismhm  13768  mhmpropd  13773  issubm  13779  issubg  13976  eqglact  14028  eqgid  14029  ecqusaddd  14041  ecqusaddcl  14042  isrng  14233  issrg  14269  srglmhm  14297  srgrmhm  14298  isring  14304  ringlghm  14366  dfrhm2  14461  issubrng  14507  issubrg3  14555  islmod  14627  islssm  14694  islssmg  14695  lsspropdg  14768  qusmulrng  14869  lmbrf  15316  uptx  15375  txcn  15376  xmetec  15538  bl2ioo  15651  lgsmodeq  16164  lgsmulsqcoprm  16165  uspgredg2v  16462  wksfval  16563  wlkeq  16595  isclwwlk  16635  clwwlkbp  16636  isclwwlknx  16657  clwwlknp  16658  clwwlkn1  16659  clwwlkn2  16662  clwwlknonel  16673  findset  16971