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

Theorem 3anass 924
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 922 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 anass 393 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
31, 2bitri 182 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wa 102  wb 103  w3a 920
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 922
This theorem is referenced by:  3anrot  925  3anan12  932  anandi3  933  3exdistr  1834  r3al  2409  ceqsex2  2640  ceqsex3v  2642  ceqsex4v  2643  ceqsex6v  2644  ceqsex8v  2645  trel3  3891  sowlin  4083  dff1o4  5165  mpt2xopovel  5890  dfsmo2  5936  ecopovtrn  6269  ecopovtrng  6272  eqinfti  6492  distrnqg  6639  recmulnqg  6643  ltexnqq  6660  enq0tr  6686  distrnq0  6711  genpdflem  6759  distrlem1prl  6834  distrlem1pru  6835  divmulasscomap  7851  muldivdirap  7862  divmuldivap  7867  prime  8527  eluz2  8706  raluz2  8748  elixx1  8996  elixx3g  9000  elioo2  9020  elioo5  9032  elicc4  9039  iccneg  9087  icoshft  9088  elfz1  9110  elfz  9111  elfz2  9112  elfzm11  9184  elfz2nn0  9205  elfzo2  9237  elfzo3  9249  lbfzo0  9267  fzind2  9325  zmodid2  9434  redivap  9899  imdivap  9906  maxleast  10237  dfgcd2  10547  lcmneg  10600  coprmgcdb  10614  divgcdcoprmex  10628  cncongr1  10629  cncongr2  10630  findset  10898
  Copyright terms: Public domain W3C validator