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

Theorem 3anass 967
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 965 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∧ 𝜒))
2 anass 399 . 2 (((𝜑𝜓) ∧ 𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
31, 2bitri 183 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∧ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wa 103  wb 104  w3a 963
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116  df-3an 965
This theorem is referenced by:  3anrot  968  3anan12  975  anandi3  976  3exdistr  1888  r3al  2478  ceqsex2  2727  ceqsex3v  2729  ceqsex4v  2730  ceqsex6v  2731  ceqsex8v  2732  eldifpr  3555  rexdifpr  3556  trel3  4038  sowlin  4246  dff1o4  5379  mpoxopovel  6142  dfsmo2  6188  ecopovtrn  6530  ecopovtrng  6533  elixp2  6600  elixp  6603  mptelixpg  6632  eqinfti  6911  distrnqg  7215  recmulnqg  7219  ltexnqq  7236  enq0tr  7262  distrnq0  7287  genpdflem  7335  distrlem1prl  7410  distrlem1pru  7411  divmulasscomap  8476  muldivdirap  8487  divmuldivap  8492  prime  9170  eluz2  9352  raluz2  9397  elixx1  9706  elixx3g  9710  elioo2  9730  elioo5  9742  elicc4  9749  iccneg  9798  icoshft  9799  elfz1  9822  elfz  9823  elfz2  9824  elfzm11  9898  elfz2nn0  9919  elfzo2  9954  elfzo3  9967  lbfzo0  9985  fzind2  10043  zmodid2  10152  redivap  10674  imdivap  10681  maxleast  11013  cosmul  11479  dfgcd2  11729  lcmneg  11782  coprmgcdb  11796  divgcdcoprmex  11810  cncongr1  11811  cncongr2  11812  lmbrf  12414  uptx  12473  txcn  12474  xmetec  12636  bl2ioo  12741  findset  13297
  Copyright terms: Public domain W3C validator