Theorem 3anass 1009

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

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

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 1007

This theorem is referenced by:  3anrot  1010  3anan12  1017  anandi3  1018  3biant1d  1392  3exdistr  1964  r3al  2577  ceqsex2  2845  ceqsex3v  2847  ceqsex4v  2848  ceqsex6v  2849  ceqsex8v  2850  eldifpr  3700  rexdifpr  3701  trel3  4200  sowlin  4423  dff1o4  5600  mpoxopovel  6450  dfsmo2  6496  ecopovtrn  6844  ecopovtrng  6847  elixp2  6914  elixp  6917  mptelixpg  6946  eqinfti  7279  distrnqg  7667  recmulnqg  7671  ltexnqq  7688  enq0tr  7714  distrnq0  7739  genpdflem  7787  distrlem1prl  7862  distrlem1pru  7863  divmulasscomap  8935  muldivdirap  8946  divmuldivap  8951  prime  9640  eluz2  9822  raluz2  9874  elixx1  10193  elixx3g  10197  elioo2  10217  elioo5  10229  elicc4  10236  iccneg  10285  icoshft  10286  elfz1  10310  elfz  10311  elfz2  10312  elfzm11  10388  elfz2nn0  10409  elfzo2  10447  elfzo3  10461  lbfzo0  10482  fzind2  10548  zmodid2  10677  swrdccatin1  11372  swrdccat  11382  redivap  11514  imdivap  11521  maxleast  11853  cosmul  12386  bitsval  12584  bitsmod  12597  bitscmp  12599  dfgcd2  12665  lcmneg  12726  coprmgcdb  12740  divgcdcoprmex  12754  cncongr1  12755  cncongr2  12756  difsqpwdvds  12991  elgz  13024  xpsfrnel  13507  xpsfrnel2  13509  mgmsscl  13524  ismhm  13624  mhmpropd  13629  issubm  13635  issubg  13840  eqglact  13892  eqgid  13893  ecqusaddd  13905  ecqusaddcl  13906  isrng  14028  issrg  14059  srglmhm  14087  srgrmhm  14088  isring  14094  ringlghm  14155  dfrhm2  14249  issubrng  14294  issubrg3  14342  islmod  14387  islssm  14453  islssmg  14454  lsspropdg  14527  qusmulrng  14628  lmbrf  15026  uptx  15085  txcn  15086  xmetec  15248  bl2ioo  15361  lgsmodeq  15864  lgsmulsqcoprm  15865  uspgredg2v  16162  wksfval  16263  wlkeq  16295  isclwwlk  16335  clwwlkbp  16336  isclwwlknx  16357  clwwlknp  16358  clwwlkn1  16359  clwwlkn2  16362  clwwlknonel  16373  findset  16661