Theorem 3anass 984

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

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

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 982

This theorem is referenced by:  3anrot  985  3anan12  992  anandi3  993  3exdistr  1930  r3al  2541  ceqsex2  2804  ceqsex3v  2806  ceqsex4v  2807  ceqsex6v  2808  ceqsex8v  2809  eldifpr  3650  rexdifpr  3651  trel3  4140  sowlin  4356  dff1o4  5515  mpoxopovel  6308  dfsmo2  6354  ecopovtrn  6700  ecopovtrng  6703  elixp2  6770  elixp  6773  mptelixpg  6802  eqinfti  7095  distrnqg  7471  recmulnqg  7475  ltexnqq  7492  enq0tr  7518  distrnq0  7543  genpdflem  7591  distrlem1prl  7666  distrlem1pru  7667  divmulasscomap  8740  muldivdirap  8751  divmuldivap  8756  prime  9442  eluz2  9624  raluz2  9670  elixx1  9989  elixx3g  9993  elioo2  10013  elioo5  10025  elicc4  10032  iccneg  10081  icoshft  10082  elfz1  10105  elfz  10106  elfz2  10107  elfzm11  10183  elfz2nn0  10204  elfzo2  10242  elfzo3  10256  lbfzo0  10274  fzind2  10332  zmodid2  10461  redivap  11056  imdivap  11063  maxleast  11395  cosmul  11927  bitsval  12125  bitsmod  12138  bitscmp  12140  dfgcd2  12206  lcmneg  12267  coprmgcdb  12281  divgcdcoprmex  12295  cncongr1  12296  cncongr2  12297  difsqpwdvds  12532  elgz  12565  xpsfrnel  13046  xpsfrnel2  13048  mgmsscl  13063  ismhm  13163  mhmpropd  13168  issubm  13174  issubg  13379  eqglact  13431  eqgid  13432  ecqusaddd  13444  ecqusaddcl  13445  isrng  13566  issrg  13597  srglmhm  13625  srgrmhm  13626  isring  13632  ringlghm  13693  dfrhm2  13786  issubrng  13831  issubrg3  13879  islmod  13923  islssm  13989  islssmg  13990  lsspropdg  14063  qusmulrng  14164  lmbrf  14535  uptx  14594  txcn  14595  xmetec  14757  bl2ioo  14870  lgsmodeq  15370  lgsmulsqcoprm  15371  findset  15675