Theorem 3anass 983

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

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

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 981

This theorem is referenced by:  3anrot  984  3anan12  991  anandi3  992  3exdistr  1925  r3al  2531  ceqsex2  2789  ceqsex3v  2791  ceqsex4v  2792  ceqsex6v  2793  ceqsex8v  2794  eldifpr  3631  rexdifpr  3632  trel3  4121  sowlin  4332  dff1o4  5481  mpoxopovel  6256  dfsmo2  6302  ecopovtrn  6646  ecopovtrng  6649  elixp2  6716  elixp  6719  mptelixpg  6748  eqinfti  7033  distrnqg  7400  recmulnqg  7404  ltexnqq  7421  enq0tr  7447  distrnq0  7472  genpdflem  7520  distrlem1prl  7595  distrlem1pru  7596  divmulasscomap  8667  muldivdirap  8678  divmuldivap  8683  prime  9366  eluz2  9548  raluz2  9593  elixx1  9911  elixx3g  9915  elioo2  9935  elioo5  9947  elicc4  9954  iccneg  10003  icoshft  10004  elfz1  10027  elfz  10028  elfz2  10029  elfzm11  10105  elfz2nn0  10126  elfzo2  10164  elfzo3  10177  lbfzo0  10195  fzind2  10253  zmodid2  10366  redivap  10897  imdivap  10904  maxleast  11236  cosmul  11767  dfgcd2  12029  lcmneg  12088  coprmgcdb  12102  divgcdcoprmex  12116  cncongr1  12117  cncongr2  12118  difsqpwdvds  12351  elgz  12383  xpsfrnel  12782  xpsfrnel2  12784  mgmsscl  12799  ismhm  12875  mhmpropd  12879  issubm  12885  issubg  13065  eqglact  13117  eqgid  13118  isrng  13186  issrg  13217  srglmhm  13245  srgrmhm  13246  isring  13252  issubrng  13419  issubrg3  13467  islmod  13480  islssm  13546  islssmg  13547  lsspropdg  13620  qusmulrng  13719  lmbrf  14011  uptx  14070  txcn  14071  xmetec  14233  bl2ioo  14338  lgsmodeq  14742  lgsmulsqcoprm  14743  findset  14993