Theorem 3anass 984

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

Syntax hints:   ∧ wa 104   ↔ wb 105   ∧ w3a 980

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

This theorem depends on definitions:  df-bi 117  df-3an 982

This theorem is referenced by:  3anrot  985  3anan12  992  anandi3  993  3exdistr  1927  r3al  2538  ceqsex2  2800  ceqsex3v  2802  ceqsex4v  2803  ceqsex6v  2804  ceqsex8v  2805  eldifpr  3645  rexdifpr  3646  trel3  4135  sowlin  4351  dff1o4  5508  mpoxopovel  6294  dfsmo2  6340  ecopovtrn  6686  ecopovtrng  6689  elixp2  6756  elixp  6759  mptelixpg  6788  eqinfti  7079  distrnqg  7447  recmulnqg  7451  ltexnqq  7468  enq0tr  7494  distrnq0  7519  genpdflem  7567  distrlem1prl  7642  distrlem1pru  7643  divmulasscomap  8715  muldivdirap  8726  divmuldivap  8731  prime  9416  eluz2  9598  raluz2  9644  elixx1  9963  elixx3g  9967  elioo2  9987  elioo5  9999  elicc4  10006  iccneg  10055  icoshft  10056  elfz1  10079  elfz  10080  elfz2  10081  elfzm11  10157  elfz2nn0  10178  elfzo2  10216  elfzo3  10230  lbfzo0  10248  fzind2  10306  zmodid2  10423  redivap  11018  imdivap  11025  maxleast  11357  cosmul  11888  dfgcd2  12151  lcmneg  12212  coprmgcdb  12226  divgcdcoprmex  12240  cncongr1  12241  cncongr2  12242  difsqpwdvds  12476  elgz  12509  xpsfrnel  12927  xpsfrnel2  12929  mgmsscl  12944  ismhm  13033  mhmpropd  13038  issubm  13044  issubg  13243  eqglact  13295  eqgid  13296  ecqusaddd  13308  ecqusaddcl  13309  isrng  13430  issrg  13461  srglmhm  13489  srgrmhm  13490  isring  13496  ringlghm  13557  dfrhm2  13650  issubrng  13695  issubrg3  13743  islmod  13787  islssm  13853  islssmg  13854  lsspropdg  13927  qusmulrng  14028  lmbrf  14383  uptx  14442  txcn  14443  xmetec  14605  bl2ioo  14710  lgsmodeq  15161  lgsmulsqcoprm  15162  findset  15437