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  4239  sowlin  4467  dff1o4  5650  mpoxopovel  6516  dfsmo2  6562  ecopovtrn  6910  ecopovtrng  6913  elixp2  6988  elixp  6991  mptelixpg  7020  eqinfti  7366  distrnqg  7760  recmulnqg  7764  ltexnqq  7781  enq0tr  7807  distrnq0  7832  genpdflem  7880  distrlem1prl  7955  distrlem1pru  7956  divmulasscomap  9034  muldivdirap  9045  divmuldivap  9050  prime  9756  eluz2  9943  raluz2  9995  elixx1  10316  elixx3g  10320  elioo2  10340  elioo5  10352  elicc4  10359  iccneg  10408  icoshft  10409  elfz1  10433  elfz  10434  elfz2  10435  elfzm11  10515  elfz2nn0  10536  elfzo2  10574  elfzo3  10588  lbfzo0  10609  fzind2  10675  zmodid2  10810  swrdccatin1  11519  swrdccat  11529  redivap  11661  imdivap  11668  maxleast  12002  cosmul  12537  bitsval  12735  bitsmod  12748  bitscmp  12750  dfgcd2  12816  lcmneg  12877  coprmgcdb  12891  divgcdcoprmex  12905  cncongr1  12906  cncongr2  12907  difsqpwdvds  13146  elgz  13179  xpsfrnel  13724  xpsfrnel2  13726  mgmsscl  13740  ismhm  13827  mhmpropd  13832  issubm  13838  issubg  14035  eqglact  14087  eqgid  14088  ecqusaddd  14100  ecqusaddcl  14101  isrng  14340  issrg  14376  srglmhm  14404  srgrmhm  14405  isring  14411  ringlghm  14473  dfrhm2  14570  issubrng  14616  issubrg3  14664  islmod  14736  islssm  14803  islssmg  14804  lsspropdg  14877  qusmulrng  14978  lmbrf  15441  uptx  15500  txcn  15501  xmetec  15663  bl2ioo  15776  lgsmodeq  16369  lgsmulsqcoprm  16370  uspgredg2v  16667  wksfval  16768  wlkeq  16800  isclwwlk  16840  clwwlkbp  16841  isclwwlknx  16862  clwwlknp  16863  clwwlkn1  16864  clwwlkn2  16867  clwwlknonel  16878  findset  17176