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  2841  ceqsex3v  2843  ceqsex4v  2844  ceqsex6v  2845  ceqsex8v  2846  eldifpr  3693  rexdifpr  3694  trel3  4190  sowlin  4411  dff1o4  5582  mpoxopovel  6393  dfsmo2  6439  ecopovtrn  6787  ecopovtrng  6790  elixp2  6857  elixp  6860  mptelixpg  6889  eqinfti  7198  distrnqg  7585  recmulnqg  7589  ltexnqq  7606  enq0tr  7632  distrnq0  7657  genpdflem  7705  distrlem1prl  7780  distrlem1pru  7781  divmulasscomap  8854  muldivdirap  8865  divmuldivap  8870  prime  9557  eluz2  9739  raluz2  9786  elixx1  10105  elixx3g  10109  elioo2  10129  elioo5  10141  elicc4  10148  iccneg  10197  icoshft  10198  elfz1  10221  elfz  10222  elfz2  10223  elfzm11  10299  elfz2nn0  10320  elfzo2  10358  elfzo3  10372  lbfzo0  10393  fzind2  10457  zmodid2  10586  swrdccatin1  11273  swrdccat  11283  redivap  11401  imdivap  11408  maxleast  11740  cosmul  12272  bitsval  12470  bitsmod  12483  bitscmp  12485  dfgcd2  12551  lcmneg  12612  coprmgcdb  12626  divgcdcoprmex  12640  cncongr1  12641  cncongr2  12642  difsqpwdvds  12877  elgz  12910  xpsfrnel  13393  xpsfrnel2  13395  mgmsscl  13410  ismhm  13510  mhmpropd  13515  issubm  13521  issubg  13726  eqglact  13778  eqgid  13779  ecqusaddd  13791  ecqusaddcl  13792  isrng  13913  issrg  13944  srglmhm  13972  srgrmhm  13973  isring  13979  ringlghm  14040  dfrhm2  14134  issubrng  14179  issubrg3  14227  islmod  14271  islssm  14337  islssmg  14338  lsspropdg  14411  qusmulrng  14512  lmbrf  14905  uptx  14964  txcn  14965  xmetec  15127  bl2ioo  15240  lgsmodeq  15740  lgsmulsqcoprm  15741  uspgredg2v  16035  wksfval  16068  wlkeq  16100  isclwwlk  16137  clwwlkbp  16138  isclwwlknx  16158  clwwlknp  16159  clwwlkn1  16160  clwwlkn2  16163  findset  16391