Theorem 3anass 1006

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

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

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 1004

This theorem is referenced by:  3anrot  1007  3anan12  1014  anandi3  1015  3biant1d  1389  3exdistr  1962  r3al  2574  ceqsex2  2841  ceqsex3v  2843  ceqsex4v  2844  ceqsex6v  2845  ceqsex8v  2846  eldifpr  3693  rexdifpr  3694  trel3  4190  sowlin  4411  dff1o4  5580  mpoxopovel  6387  dfsmo2  6433  ecopovtrn  6779  ecopovtrng  6782  elixp2  6849  elixp  6852  mptelixpg  6881  eqinfti  7187  distrnqg  7574  recmulnqg  7578  ltexnqq  7595  enq0tr  7621  distrnq0  7646  genpdflem  7694  distrlem1prl  7769  distrlem1pru  7770  divmulasscomap  8843  muldivdirap  8854  divmuldivap  8859  prime  9546  eluz2  9728  raluz2  9774  elixx1  10093  elixx3g  10097  elioo2  10117  elioo5  10129  elicc4  10136  iccneg  10185  icoshft  10186  elfz1  10209  elfz  10210  elfz2  10211  elfzm11  10287  elfz2nn0  10308  elfzo2  10346  elfzo3  10360  lbfzo0  10381  fzind2  10445  zmodid2  10574  swrdccatin1  11257  swrdccat  11267  redivap  11385  imdivap  11392  maxleast  11724  cosmul  12256  bitsval  12454  bitsmod  12467  bitscmp  12469  dfgcd2  12535  lcmneg  12596  coprmgcdb  12610  divgcdcoprmex  12624  cncongr1  12625  cncongr2  12626  difsqpwdvds  12861  elgz  12894  xpsfrnel  13377  xpsfrnel2  13379  mgmsscl  13394  ismhm  13494  mhmpropd  13499  issubm  13505  issubg  13710  eqglact  13762  eqgid  13763  ecqusaddd  13775  ecqusaddcl  13776  isrng  13897  issrg  13928  srglmhm  13956  srgrmhm  13957  isring  13963  ringlghm  14024  dfrhm2  14118  issubrng  14163  issubrg3  14211  islmod  14255  islssm  14321  islssmg  14322  lsspropdg  14395  qusmulrng  14496  lmbrf  14889  uptx  14948  txcn  14949  xmetec  15111  bl2ioo  15224  lgsmodeq  15724  lgsmulsqcoprm  15725  uspgredg2v  16019  wksfval  16035  wlkeq  16065  findset  16308