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  1927  r3al  2538  ceqsex2  2801  ceqsex3v  2803  ceqsex4v  2804  ceqsex6v  2805  ceqsex8v  2806  eldifpr  3646  rexdifpr  3647  trel3  4136  sowlin  4352  dff1o4  5509  mpoxopovel  6296  dfsmo2  6342  ecopovtrn  6688  ecopovtrng  6691  elixp2  6758  elixp  6761  mptelixpg  6790  eqinfti  7081  distrnqg  7449  recmulnqg  7453  ltexnqq  7470  enq0tr  7496  distrnq0  7521  genpdflem  7569  distrlem1prl  7644  distrlem1pru  7645  divmulasscomap  8717  muldivdirap  8728  divmuldivap  8733  prime  9419  eluz2  9601  raluz2  9647  elixx1  9966  elixx3g  9970  elioo2  9990  elioo5  10002  elicc4  10009  iccneg  10058  icoshft  10059  elfz1  10082  elfz  10083  elfz2  10084  elfzm11  10160  elfz2nn0  10181  elfzo2  10219  elfzo3  10233  lbfzo0  10251  fzind2  10309  zmodid2  10426  redivap  11021  imdivap  11028  maxleast  11360  cosmul  11891  dfgcd2  12154  lcmneg  12215  coprmgcdb  12229  divgcdcoprmex  12243  cncongr1  12244  cncongr2  12245  difsqpwdvds  12479  elgz  12512  xpsfrnel  12930  xpsfrnel2  12932  mgmsscl  12947  ismhm  13036  mhmpropd  13041  issubm  13047  issubg  13246  eqglact  13298  eqgid  13299  ecqusaddd  13311  ecqusaddcl  13312  isrng  13433  issrg  13464  srglmhm  13492  srgrmhm  13493  isring  13499  ringlghm  13560  dfrhm2  13653  issubrng  13698  issubrg3  13746  islmod  13790  islssm  13856  islssmg  13857  lsspropdg  13930  qusmulrng  14031  lmbrf  14394  uptx  14453  txcn  14454  xmetec  14616  bl2ioo  14729  lgsmodeq  15202  lgsmulsqcoprm  15203  findset  15507