Theorem 3anass 985

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

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

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 983

This theorem is referenced by:  3anrot  986  3anan12  993  anandi3  994  3biant1d  1367  3exdistr  1939  r3al  2550  ceqsex2  2813  ceqsex3v  2815  ceqsex4v  2816  ceqsex6v  2817  ceqsex8v  2818  eldifpr  3660  rexdifpr  3661  trel3  4150  sowlin  4367  dff1o4  5530  mpoxopovel  6327  dfsmo2  6373  ecopovtrn  6719  ecopovtrng  6722  elixp2  6789  elixp  6792  mptelixpg  6821  eqinfti  7122  distrnqg  7500  recmulnqg  7504  ltexnqq  7521  enq0tr  7547  distrnq0  7572  genpdflem  7620  distrlem1prl  7695  distrlem1pru  7696  divmulasscomap  8769  muldivdirap  8780  divmuldivap  8785  prime  9472  eluz2  9654  raluz2  9700  elixx1  10019  elixx3g  10023  elioo2  10043  elioo5  10055  elicc4  10062  iccneg  10111  icoshft  10112  elfz1  10135  elfz  10136  elfz2  10137  elfzm11  10213  elfz2nn0  10234  elfzo2  10272  elfzo3  10286  lbfzo0  10305  fzind2  10368  zmodid2  10497  redivap  11185  imdivap  11192  maxleast  11524  cosmul  12056  bitsval  12254  bitsmod  12267  bitscmp  12269  dfgcd2  12335  lcmneg  12396  coprmgcdb  12410  divgcdcoprmex  12424  cncongr1  12425  cncongr2  12426  difsqpwdvds  12661  elgz  12694  xpsfrnel  13176  xpsfrnel2  13178  mgmsscl  13193  ismhm  13293  mhmpropd  13298  issubm  13304  issubg  13509  eqglact  13561  eqgid  13562  ecqusaddd  13574  ecqusaddcl  13575  isrng  13696  issrg  13727  srglmhm  13755  srgrmhm  13756  isring  13762  ringlghm  13823  dfrhm2  13916  issubrng  13961  issubrg3  14009  islmod  14053  islssm  14119  islssmg  14120  lsspropdg  14193  qusmulrng  14294  lmbrf  14687  uptx  14746  txcn  14747  xmetec  14909  bl2ioo  15022  lgsmodeq  15522  lgsmulsqcoprm  15523  findset  15881