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

Theorem 3anass 888
 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 886 . 2 ((φ ψ χ) ↔ ((φ ψ) χ))
2 anass 381 . 2 (((φ ψ) χ) ↔ (φ (ψ χ)))
31, 2bitri 173 1 ((φ ψ χ) ↔ (φ (ψ χ)))
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98   ∧ w3a 884 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101 This theorem depends on definitions:  df-bi 110  df-3an 886 This theorem is referenced by:  3anrot  889  3anan12  896  anandi3  897  3exdistr  1789  r3al  2360  ceqsex2  2588  ceqsex3v  2590  ceqsex4v  2591  ceqsex6v  2592  ceqsex8v  2593  trel3  3853  sowlin  4048  dff1o4  5077  mpt2xopovel  5797  dfsmo2  5843  ecopovtrn  6139  ecopovtrng  6142  distrnqg  6371  recmulnqg  6375  ltexnqq  6391  enq0tr  6417  distrnq0  6442  genpdflem  6490  distrlem1prl  6558  distrlem1pru  6559  divmuldivap  7470  prime  8113  eluz2  8255  raluz2  8298  elixx1  8536  elixx3g  8540  elioo2  8560  elioo5  8572  elicc4  8579  iccneg  8627  icoshft  8628  elfz1  8649  elfz  8650  elfz2  8651  elfzm11  8723  elfz2nn0  8743  elfzo2  8777  elfzo3  8789  lbfzo0  8807  fzind2  8865  redivap  9102  imdivap  9109  findset  9405
 Copyright terms: Public domain W3C validator