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  6406  dfsmo2  6452  ecopovtrn  6800  ecopovtrng  6803  elixp2  6870  elixp  6873  mptelixpg  6902  eqinfti  7218  distrnqg  7606  recmulnqg  7610  ltexnqq  7627  enq0tr  7653  distrnq0  7678  genpdflem  7726  distrlem1prl  7801  distrlem1pru  7802  divmulasscomap  8875  muldivdirap  8886  divmuldivap  8891  prime  9578  eluz2  9760  raluz2  9812  elixx1  10131  elixx3g  10135  elioo2  10155  elioo5  10167  elicc4  10174  iccneg  10223  icoshft  10224  elfz1  10247  elfz  10248  elfz2  10249  elfzm11  10325  elfz2nn0  10346  elfzo2  10384  elfzo3  10398  lbfzo0  10419  fzind2  10484  zmodid2  10613  swrdccatin1  11305  swrdccat  11315  redivap  11434  imdivap  11441  maxleast  11773  cosmul  12305  bitsval  12503  bitsmod  12516  bitscmp  12518  dfgcd2  12584  lcmneg  12645  coprmgcdb  12659  divgcdcoprmex  12673  cncongr1  12674  cncongr2  12675  difsqpwdvds  12910  elgz  12943  xpsfrnel  13426  xpsfrnel2  13428  mgmsscl  13443  ismhm  13543  mhmpropd  13548  issubm  13554  issubg  13759  eqglact  13811  eqgid  13812  ecqusaddd  13824  ecqusaddcl  13825  isrng  13946  issrg  13977  srglmhm  14005  srgrmhm  14006  isring  14012  ringlghm  14073  dfrhm2  14167  issubrng  14212  issubrg3  14260  islmod  14304  islssm  14370  islssmg  14371  lsspropdg  14444  qusmulrng  14545  lmbrf  14938  uptx  14997  txcn  14998  xmetec  15160  bl2ioo  15273  lgsmodeq  15773  lgsmulsqcoprm  15774  uspgredg2v  16071  wksfval  16172  wlkeq  16204  isclwwlk  16244  clwwlkbp  16245  isclwwlknx  16266  clwwlknp  16267  clwwlkn1  16268  clwwlkn2  16271  clwwlknonel  16282  findset  16540