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  7361  distrnqg  7755  recmulnqg  7759  ltexnqq  7776  enq0tr  7802  distrnq0  7827  genpdflem  7875  distrlem1prl  7950  distrlem1pru  7951  divmulasscomap  9029  muldivdirap  9040  divmuldivap  9045  prime  9750  eluz2  9937  raluz2  9989  elixx1  10310  elixx3g  10314  elioo2  10334  elioo5  10346  elicc4  10353  iccneg  10402  icoshft  10403  elfz1  10427  elfz  10428  elfz2  10429  elfzm11  10509  elfz2nn0  10530  elfzo2  10568  elfzo3  10582  lbfzo0  10603  fzind2  10669  zmodid2  10804  swrdccatin1  11513  swrdccat  11523  redivap  11655  imdivap  11662  maxleast  11996  cosmul  12531  bitsval  12729  bitsmod  12742  bitscmp  12744  dfgcd2  12810  lcmneg  12871  coprmgcdb  12885  divgcdcoprmex  12899  cncongr1  12900  cncongr2  12901  difsqpwdvds  13140  elgz  13173  xpsfrnel  13718  xpsfrnel2  13720  mgmsscl  13734  ismhm  13821  mhmpropd  13826  issubm  13832  issubg  14029  eqglact  14081  eqgid  14082  ecqusaddd  14094  ecqusaddcl  14095  isrng  14317  issrg  14353  srglmhm  14381  srgrmhm  14382  isring  14388  ringlghm  14450  dfrhm2  14545  issubrng  14591  issubrg3  14639  islmod  14711  islssm  14778  islssmg  14779  lsspropdg  14852  qusmulrng  14953  lmbrf  15407  uptx  15466  txcn  15467  xmetec  15629  bl2ioo  15742  lgsmodeq  16330  lgsmulsqcoprm  16331  uspgredg2v  16628  wksfval  16729  wlkeq  16761  isclwwlk  16801  clwwlkbp  16802  isclwwlknx  16823  clwwlknp  16824  clwwlkn1  16825  clwwlkn2  16828  clwwlknonel  16839  findset  17137