Theorem 3anass 1013

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

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anrot  1014  3anan12  1021  anandi3  1022  3biant1d  1396  3exdistr  1971  r3al  2594  ceqsex2  2863  ceqsex3v  2865  ceqsex4v  2866  ceqsex6v  2867  ceqsex8v  2868  eldifpr  3736  rexdifpr  3737  trel3  4237  sowlin  4465  dff1o4  5647  mpoxopovel  6512  dfsmo2  6558  ecopovtrn  6906  ecopovtrng  6909  elixp2  6984  elixp  6987  mptelixpg  7016  eqinfti  7360  distrnqg  7754  recmulnqg  7758  ltexnqq  7775  enq0tr  7801  distrnq0  7826  genpdflem  7874  distrlem1prl  7949  distrlem1pru  7950  divmulasscomap  9028  muldivdirap  9039  divmuldivap  9044  prime  9749  eluz2  9936  raluz2  9988  elixx1  10309  elixx3g  10313  elioo2  10333  elioo5  10345  elicc4  10352  iccneg  10401  icoshft  10402  elfz1  10426  elfz  10427  elfz2  10428  elfzm11  10508  elfz2nn0  10529  elfzo2  10567  elfzo3  10581  lbfzo0  10602  fzind2  10668  zmodid2  10802  swrdccatin1  11511  swrdccat  11521  redivap  11653  imdivap  11660  maxleast  11994  cosmul  12528  bitsval  12726  bitsmod  12739  bitscmp  12741  dfgcd2  12807  lcmneg  12868  coprmgcdb  12882  divgcdcoprmex  12896  cncongr1  12897  cncongr2  12898  difsqpwdvds  13137  elgz  13170  xpsfrnel  13714  xpsfrnel2  13716  mgmsscl  13730  ismhm  13817  mhmpropd  13822  issubm  13828  issubg  14025  eqglact  14077  eqgid  14078  ecqusaddd  14090  ecqusaddcl  14091  isrng  14282  issrg  14318  srglmhm  14346  srgrmhm  14347  isring  14353  ringlghm  14415  dfrhm2  14510  issubrng  14556  issubrg3  14604  islmod  14676  islssm  14743  islssmg  14744  lsspropdg  14817  qusmulrng  14918  lmbrf  15365  uptx  15424  txcn  15425  xmetec  15587  bl2ioo  15700  lgsmodeq  16262  lgsmulsqcoprm  16263  uspgredg2v  16560  wksfval  16661  wlkeq  16693  isclwwlk  16733  clwwlkbp  16734  isclwwlknx  16755  clwwlknp  16756  clwwlkn1  16757  clwwlkn2  16760  clwwlknonel  16771  findset  17069