Theorem 3anass 1013

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

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105   ∧ w3a 1009

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117  df-3an 1011

This theorem is used by:  3anrot  1014  3anan12  1021  anandi3  1022  3biant1d  1396  3exdistr  1971  r3al  2594  ceqsex2  2863  ceqsex3v  2865  ceqsex4v  2866  ceqsex6v  2867  ceqsex8v  2868  eldifpr  3736  rexdifpr  3737  trel3  4239  sowlin  4467  dff1o4  5650  mpoxopovel  6517  dfsmo2  6563  ecopovtrn  6911  ecopovtrng  6914  elixp2  6990  elixp  6993  mptelixpg  7022  eqinfti  7366  distrnqg  7760  recmulnqg  7764  ltexnqq  7781  enq0tr  7807  distrnq0  7832  genpdflem  7880  distrlem1prl  7955  distrlem1pru  7956  divmulasscomap  9034  muldivdirap  9045  divmuldivap  9050  prime  9755  eluz2  9942  raluz2  9994  elixx1  10315  elixx3g  10319  elioo2  10339  elioo5  10351  elicc4  10358  iccneg  10407  icoshft  10408  elfz1  10432  elfz  10433  elfz2  10434  elfzm11  10514  elfz2nn0  10535  elfzo2  10573  elfzo3  10587  lbfzo0  10608  fzind2  10674  zmodid2  10809  swrdccatin1  11518  swrdccat  11528  redivap  11660  imdivap  11667  maxleast  12001  cosmul  12536  bitsval  12734  bitsmod  12747  bitscmp  12749  dfgcd2  12815  lcmneg  12876  coprmgcdb  12890  divgcdcoprmex  12904  cncongr1  12905  cncongr2  12906  difsqpwdvds  13145  elgz  13178  xpsfrnel  13723  xpsfrnel2  13725  mgmsscl  13739  ismhm  13826  mhmpropd  13831  issubm  13837  issubg  14034  eqglact  14086  eqgid  14087  ecqusaddd  14099  ecqusaddcl  14100  isrng  14339  issrg  14375  srglmhm  14403  srgrmhm  14404  isring  14410  ringlghm  14472  dfrhm2  14569  issubrng  14615  issubrg3  14663  islmod  14735  islssm  14802  islssmg  14803  lsspropdg  14876  qusmulrng  14977  lmbrf  15458  uptx  15517  txcn  15518  xmetec  15680  bl2ioo  15793  lgsmodeq  16386  lgsmulsqcoprm  16387  uspgredg2v  16684  wksfval  16785  wlkeq  16817  isclwwlk  16857  clwwlkbp  16858  isclwwlknx  16879  clwwlknp  16880  clwwlkn1  16881  clwwlkn2  16884  clwwlknonel  16895  findset  17193