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 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) ↔ (𝜑 ∧ (𝜓 ∧ 𝜒)))

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

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 1011

This theorem is referenced by:  3anrot  1014  3anan12  1021  anandi3  1022  3biant1d  1396  3exdistr  1971  r3al  2594  ceqsex2  2863  ceqsex3v  2865  ceqsex4v  2866  ceqsex6v  2867  ceqsex8v  2868  eldifpr  3732  rexdifpr  3733  trel3  4232  sowlin  4460  dff1o4  5642  mpoxopovel  6502  dfsmo2  6548  ecopovtrn  6896  ecopovtrng  6899  elixp2  6974  elixp  6977  mptelixpg  7006  eqinfti  7350  distrnqg  7744  recmulnqg  7748  ltexnqq  7765  enq0tr  7791  distrnq0  7816  genpdflem  7864  distrlem1prl  7939  distrlem1pru  7940  divmulasscomap  9016  muldivdirap  9027  divmuldivap  9032  prime  9724  eluz2  9906  raluz2  9958  elixx1  10278  elixx3g  10282  elioo2  10302  elioo5  10314  elicc4  10321  iccneg  10370  icoshft  10371  elfz1  10395  elfz  10396  elfz2  10397  elfzm11  10476  elfz2nn0  10497  elfzo2  10535  elfzo3  10549  lbfzo0  10570  fzind2  10636  zmodid2  10767  swrdccatin1  11475  swrdccat  11485  redivap  11617  imdivap  11624  maxleast  11957  cosmul  12490  bitsval  12688  bitsmod  12701  bitscmp  12703  dfgcd2  12769  lcmneg  12830  coprmgcdb  12844  divgcdcoprmex  12858  cncongr1  12859  cncongr2  12860  difsqpwdvds  13095  elgz  13128  xpsfrnel  13642  xpsfrnel2  13644  mgmsscl  13658  ismhm  13745  mhmpropd  13750  issubm  13756  issubg  13953  eqglact  14005  eqgid  14006  ecqusaddd  14018  ecqusaddcl  14019  isrng  14208  issrg  14243  srglmhm  14271  srgrmhm  14272  isring  14278  ringlghm  14339  dfrhm2  14434  issubrng  14480  issubrg3  14528  islmod  14600  islssm  14666  islssmg  14667  lsspropdg  14740  qusmulrng  14841  lmbrf  15239  uptx  15298  txcn  15299  xmetec  15461  bl2ioo  15574  lgsmodeq  16078  lgsmulsqcoprm  16079  uspgredg2v  16376  wksfval  16477  wlkeq  16509  isclwwlk  16549  clwwlkbp  16550  isclwwlknx  16571  clwwlknp  16572  clwwlkn1  16573  clwwlkn2  16576  clwwlknonel  16587  findset  16885