Theorem 3anass 1006

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

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

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 1004

This theorem is referenced by:  3anrot  1007  3anan12  1014  anandi3  1015  3biant1d  1389  3exdistr  1962  r3al  2574  ceqsex2  2842  ceqsex3v  2844  ceqsex4v  2845  ceqsex6v  2846  ceqsex8v  2847  eldifpr  3694  rexdifpr  3695  trel3  4193  sowlin  4415  dff1o4  5588  mpoxopovel  6402  dfsmo2  6448  ecopovtrn  6796  ecopovtrng  6799  elixp2  6866  elixp  6869  mptelixpg  6898  eqinfti  7210  distrnqg  7597  recmulnqg  7601  ltexnqq  7618  enq0tr  7644  distrnq0  7669  genpdflem  7717  distrlem1prl  7792  distrlem1pru  7793  divmulasscomap  8866  muldivdirap  8877  divmuldivap  8882  prime  9569  eluz2  9751  raluz2  9803  elixx1  10122  elixx3g  10126  elioo2  10146  elioo5  10158  elicc4  10165  iccneg  10214  icoshft  10215  elfz1  10238  elfz  10239  elfz2  10240  elfzm11  10316  elfz2nn0  10337  elfzo2  10375  elfzo3  10389  lbfzo0  10410  fzind2  10475  zmodid2  10604  swrdccatin1  11296  swrdccat  11306  redivap  11425  imdivap  11432  maxleast  11764  cosmul  12296  bitsval  12494  bitsmod  12507  bitscmp  12509  dfgcd2  12575  lcmneg  12636  coprmgcdb  12650  divgcdcoprmex  12664  cncongr1  12665  cncongr2  12666  difsqpwdvds  12901  elgz  12934  xpsfrnel  13417  xpsfrnel2  13419  mgmsscl  13434  ismhm  13534  mhmpropd  13539  issubm  13545  issubg  13750  eqglact  13802  eqgid  13803  ecqusaddd  13815  ecqusaddcl  13816  isrng  13937  issrg  13968  srglmhm  13996  srgrmhm  13997  isring  14003  ringlghm  14064  dfrhm2  14158  issubrng  14203  issubrg3  14251  islmod  14295  islssm  14361  islssmg  14362  lsspropdg  14435  qusmulrng  14536  lmbrf  14929  uptx  14988  txcn  14989  xmetec  15151  bl2ioo  15264  lgsmodeq  15764  lgsmulsqcoprm  15765  uspgredg2v  16060  wksfval  16119  wlkeq  16151  isclwwlk  16189  clwwlkbp  16190  isclwwlknx  16211  clwwlknp  16212  clwwlkn1  16213  clwwlkn2  16216  clwwlknonel  16227  findset  16476