ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  3anass GIF version

Theorem 3anass 926
Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
3anass ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))

Proof of Theorem 3anass
StepHypRef Expression
1 df-3an 924 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 anass 393 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
31, 2bitri 182 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103  w3a 922
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115  df-3an 924
This theorem is referenced by:  3anrot  927  3anan12  934  anandi3  935  3exdistr  1837  r3al  2416  ceqsex2  2653  ceqsex3v  2655  ceqsex4v  2656  ceqsex6v  2657  ceqsex8v  2658  trel3  3921  sowlin  4123  dff1o4  5226  mpt2xopovel  5962  dfsmo2  6008  ecopovtrn  6343  ecopovtrng  6346  eqinfti  6662  distrnqg  6893  recmulnqg  6897  ltexnqq  6914  enq0tr  6940  distrnq0  6965  genpdflem  7013  distrlem1prl  7088  distrlem1pru  7089  divmulasscomap  8105  muldivdirap  8116  divmuldivap  8121  prime  8781  eluz2  8960  raluz2  9002  elixx1  9250  elixx3g  9254  elioo2  9274  elioo5  9286  elicc4  9293  iccneg  9341  icoshft  9342  elfz1  9364  elfz  9365  elfz2  9366  elfzm11  9438  elfz2nn0  9459  elfzo2  9492  elfzo3  9505  lbfzo0  9523  fzind2  9581  zmodid2  9690  redivap  10207  imdivap  10214  maxleast  10545  dfgcd2  10909  lcmneg  10962  coprmgcdb  10976  divgcdcoprmex  10990  cncongr1  10991  cncongr2  10992  findset  11309
  Copyright terms: Public domain W3C validator