Theorem 3anass 985

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

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

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 983

This theorem is referenced by:  3anrot  986  3anan12  993  anandi3  994  3biant1d  1367  3exdistr  1940  r3al  2552  ceqsex2  2818  ceqsex3v  2820  ceqsex4v  2821  ceqsex6v  2822  ceqsex8v  2823  eldifpr  3670  rexdifpr  3671  trel3  4166  sowlin  4385  dff1o4  5552  mpoxopovel  6350  dfsmo2  6396  ecopovtrn  6742  ecopovtrng  6745  elixp2  6812  elixp  6815  mptelixpg  6844  eqinfti  7148  distrnqg  7535  recmulnqg  7539  ltexnqq  7556  enq0tr  7582  distrnq0  7607  genpdflem  7655  distrlem1prl  7730  distrlem1pru  7731  divmulasscomap  8804  muldivdirap  8815  divmuldivap  8820  prime  9507  eluz2  9689  raluz2  9735  elixx1  10054  elixx3g  10058  elioo2  10078  elioo5  10090  elicc4  10097  iccneg  10146  icoshft  10147  elfz1  10170  elfz  10171  elfz2  10172  elfzm11  10248  elfz2nn0  10269  elfzo2  10307  elfzo3  10321  lbfzo0  10342  fzind2  10405  zmodid2  10534  swrdccatin1  11216  swrdccat  11226  redivap  11300  imdivap  11307  maxleast  11639  cosmul  12171  bitsval  12369  bitsmod  12382  bitscmp  12384  dfgcd2  12450  lcmneg  12511  coprmgcdb  12525  divgcdcoprmex  12539  cncongr1  12540  cncongr2  12541  difsqpwdvds  12776  elgz  12809  xpsfrnel  13291  xpsfrnel2  13293  mgmsscl  13308  ismhm  13408  mhmpropd  13413  issubm  13419  issubg  13624  eqglact  13676  eqgid  13677  ecqusaddd  13689  ecqusaddcl  13690  isrng  13811  issrg  13842  srglmhm  13870  srgrmhm  13871  isring  13877  ringlghm  13938  dfrhm2  14031  issubrng  14076  issubrg3  14124  islmod  14168  islssm  14234  islssmg  14235  lsspropdg  14308  qusmulrng  14409  lmbrf  14802  uptx  14861  txcn  14862  xmetec  15024  bl2ioo  15137  lgsmodeq  15637  lgsmulsqcoprm  15638  findset  16080