Theorem 3anass 982

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

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

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 980

This theorem is referenced by:  3anrot  983  3anan12  990  anandi3  991  3exdistr  1915  r3al  2521  ceqsex2  2779  ceqsex3v  2781  ceqsex4v  2782  ceqsex6v  2783  ceqsex8v  2784  eldifpr  3621  rexdifpr  3622  trel3  4111  sowlin  4322  dff1o4  5471  mpoxopovel  6245  dfsmo2  6291  ecopovtrn  6635  ecopovtrng  6638  elixp2  6705  elixp  6708  mptelixpg  6737  eqinfti  7022  distrnqg  7389  recmulnqg  7393  ltexnqq  7410  enq0tr  7436  distrnq0  7461  genpdflem  7509  distrlem1prl  7584  distrlem1pru  7585  divmulasscomap  8656  muldivdirap  8667  divmuldivap  8672  prime  9355  eluz2  9537  raluz2  9582  elixx1  9900  elixx3g  9904  elioo2  9924  elioo5  9936  elicc4  9943  iccneg  9992  icoshft  9993  elfz1  10016  elfz  10017  elfz2  10018  elfzm11  10094  elfz2nn0  10115  elfzo2  10153  elfzo3  10166  lbfzo0  10184  fzind2  10242  zmodid2  10355  redivap  10886  imdivap  10893  maxleast  11225  cosmul  11756  dfgcd2  12018  lcmneg  12077  coprmgcdb  12091  divgcdcoprmex  12105  cncongr1  12106  cncongr2  12107  difsqpwdvds  12340  elgz  12372  xpsfrnel  12770  xpsfrnel2  12772  mgmsscl  12787  ismhm  12860  mhmpropd  12864  issubm  12870  issubg  13043  eqglact  13095  eqgid  13096  issrg  13159  srglmhm  13187  srgrmhm  13188  isring  13194  issubrg3  13379  islmod  13392  islssm  13456  lsspropdg  13529  lmbrf  13876  uptx  13935  txcn  13936  xmetec  14098  bl2ioo  14203  lgsmodeq  14607  lgsmulsqcoprm  14608  findset  14858