Theorem 3anass 1009

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

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

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 1007

This theorem is referenced by:  3anrot  1010  3anan12  1017  anandi3  1018  3biant1d  1392  3exdistr  1967  r3al  2588  ceqsex2  2857  ceqsex3v  2859  ceqsex4v  2860  ceqsex6v  2861  ceqsex8v  2862  eldifpr  3721  rexdifpr  3722  trel3  4221  sowlin  4446  dff1o4  5627  mpoxopovel  6485  dfsmo2  6531  ecopovtrn  6879  ecopovtrng  6882  elixp2  6950  elixp  6953  mptelixpg  6982  eqinfti  7324  distrnqg  7718  recmulnqg  7722  ltexnqq  7739  enq0tr  7765  distrnq0  7790  genpdflem  7838  distrlem1prl  7913  distrlem1pru  7914  divmulasscomap  8987  muldivdirap  8998  divmuldivap  9003  prime  9695  eluz2  9877  raluz2  9929  elixx1  10249  elixx3g  10253  elioo2  10273  elioo5  10285  elicc4  10292  iccneg  10341  icoshft  10342  elfz1  10366  elfz  10367  elfz2  10368  elfzm11  10447  elfz2nn0  10468  elfzo2  10506  elfzo3  10520  lbfzo0  10541  fzind2  10607  zmodid2  10738  swrdccatin1  11442  swrdccat  11452  redivap  11584  imdivap  11591  maxleast  11923  cosmul  12456  bitsval  12654  bitsmod  12667  bitscmp  12669  dfgcd2  12735  lcmneg  12796  coprmgcdb  12810  divgcdcoprmex  12824  cncongr1  12825  cncongr2  12826  difsqpwdvds  13061  elgz  13094  xpsfrnel  13608  xpsfrnel2  13610  mgmsscl  13624  ismhm  13716  mhmpropd  13721  issubm  13727  issubg  13926  eqglact  13978  eqgid  13979  ecqusaddd  13991  ecqusaddcl  13992  isrng  14173  issrg  14208  srglmhm  14236  srgrmhm  14237  isring  14243  ringlghm  14304  dfrhm2  14399  issubrng  14445  issubrg3  14493  islmod  14565  islssm  14631  islssmg  14632  lsspropdg  14705  qusmulrng  14806  lmbrf  15206  uptx  15265  txcn  15266  xmetec  15428  bl2ioo  15541  lgsmodeq  16044  lgsmulsqcoprm  16045  uspgredg2v  16342  wksfval  16443  wlkeq  16475  isclwwlk  16515  clwwlkbp  16516  isclwwlknx  16537  clwwlknp  16538  clwwlkn1  16539  clwwlkn2  16542  clwwlknonel  16553  findset  16841