Theorem 3anass 984

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

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

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 982

This theorem is referenced by:  3anrot  985  3anan12  992  anandi3  993  3exdistr  1930  r3al  2541  ceqsex2  2804  ceqsex3v  2806  ceqsex4v  2807  ceqsex6v  2808  ceqsex8v  2809  eldifpr  3649  rexdifpr  3650  trel3  4139  sowlin  4355  dff1o4  5512  mpoxopovel  6299  dfsmo2  6345  ecopovtrn  6691  ecopovtrng  6694  elixp2  6761  elixp  6764  mptelixpg  6793  eqinfti  7086  distrnqg  7454  recmulnqg  7458  ltexnqq  7475  enq0tr  7501  distrnq0  7526  genpdflem  7574  distrlem1prl  7649  distrlem1pru  7650  divmulasscomap  8723  muldivdirap  8734  divmuldivap  8739  prime  9425  eluz2  9607  raluz2  9653  elixx1  9972  elixx3g  9976  elioo2  9996  elioo5  10008  elicc4  10015  iccneg  10064  icoshft  10065  elfz1  10088  elfz  10089  elfz2  10090  elfzm11  10166  elfz2nn0  10187  elfzo2  10225  elfzo3  10239  lbfzo0  10257  fzind2  10315  zmodid2  10444  redivap  11039  imdivap  11046  maxleast  11378  cosmul  11910  bitsval  12108  dfgcd2  12181  lcmneg  12242  coprmgcdb  12256  divgcdcoprmex  12270  cncongr1  12271  cncongr2  12272  difsqpwdvds  12507  elgz  12540  xpsfrnel  12987  xpsfrnel2  12989  mgmsscl  13004  ismhm  13093  mhmpropd  13098  issubm  13104  issubg  13303  eqglact  13355  eqgid  13356  ecqusaddd  13368  ecqusaddcl  13369  isrng  13490  issrg  13521  srglmhm  13549  srgrmhm  13550  isring  13556  ringlghm  13617  dfrhm2  13710  issubrng  13755  issubrg3  13803  islmod  13847  islssm  13913  islssmg  13914  lsspropdg  13987  qusmulrng  14088  lmbrf  14451  uptx  14510  txcn  14511  xmetec  14673  bl2ioo  14786  lgsmodeq  15286  lgsmulsqcoprm  15287  findset  15591