Theorem 3anass 1008

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

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

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 1006

This theorem is referenced by:  3anrot  1009  3anan12  1016  anandi3  1017  3biant1d  1391  3exdistr  1964  r3al  2576  ceqsex2  2844  ceqsex3v  2846  ceqsex4v  2847  ceqsex6v  2848  ceqsex8v  2849  eldifpr  3696  rexdifpr  3697  trel3  4195  sowlin  4417  dff1o4  5591  mpoxopovel  6407  dfsmo2  6453  ecopovtrn  6801  ecopovtrng  6804  elixp2  6871  elixp  6874  mptelixpg  6903  eqinfti  7219  distrnqg  7607  recmulnqg  7611  ltexnqq  7628  enq0tr  7654  distrnq0  7679  genpdflem  7727  distrlem1prl  7802  distrlem1pru  7803  divmulasscomap  8876  muldivdirap  8887  divmuldivap  8892  prime  9579  eluz2  9761  raluz2  9813  elixx1  10132  elixx3g  10136  elioo2  10156  elioo5  10168  elicc4  10175  iccneg  10224  icoshft  10225  elfz1  10248  elfz  10249  elfz2  10250  elfzm11  10326  elfz2nn0  10347  elfzo2  10385  elfzo3  10399  lbfzo0  10420  fzind2  10486  zmodid2  10615  swrdccatin1  11310  swrdccat  11320  redivap  11452  imdivap  11459  maxleast  11791  cosmul  12324  bitsval  12522  bitsmod  12535  bitscmp  12537  dfgcd2  12603  lcmneg  12664  coprmgcdb  12678  divgcdcoprmex  12692  cncongr1  12693  cncongr2  12694  difsqpwdvds  12929  elgz  12962  xpsfrnel  13445  xpsfrnel2  13447  mgmsscl  13462  ismhm  13562  mhmpropd  13567  issubm  13573  issubg  13778  eqglact  13830  eqgid  13831  ecqusaddd  13843  ecqusaddcl  13844  isrng  13966  issrg  13997  srglmhm  14025  srgrmhm  14026  isring  14032  ringlghm  14093  dfrhm2  14187  issubrng  14232  issubrg3  14280  islmod  14324  islssm  14390  islssmg  14391  lsspropdg  14464  qusmulrng  14565  lmbrf  14958  uptx  15017  txcn  15018  xmetec  15180  bl2ioo  15293  lgsmodeq  15793  lgsmulsqcoprm  15794  uspgredg2v  16091  wksfval  16192  wlkeq  16224  isclwwlk  16264  clwwlkbp  16265  isclwwlknx  16286  clwwlknp  16287  clwwlkn1  16288  clwwlkn2  16291  clwwlknonel  16302  findset  16591