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

Theorem 3anass 900
Description: Associative law for triple conjunction. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
3anass  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )

Proof of Theorem 3anass
StepHypRef Expression
1 df-3an 898 . 2  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ( ph  /\  ps )  /\  ch )
)
2 anass 387 . 2  |-  ( ( ( ph  /\  ps )  /\  ch )  <->  ( ph  /\  ( ps  /\  ch ) ) )
31, 2bitri 177 1  |-  ( (
ph  /\  ps  /\  ch ) 
<->  ( ph  /\  ( ps  /\  ch ) ) )
Colors of variables: wff set class
Syntax hints:    /\ wa 101    <-> wb 102    /\ w3a 896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105
This theorem depends on definitions:  df-bi 114  df-3an 898
This theorem is referenced by:  3anrot  901  3anan12  908  anandi3  909  3exdistr  1808  r3al  2383  ceqsex2  2611  ceqsex3v  2613  ceqsex4v  2614  ceqsex6v  2615  ceqsex8v  2616  trel3  3890  sowlin  4085  dff1o4  5162  mpt2xopovel  5887  dfsmo2  5933  ecopovtrn  6234  ecopovtrng  6237  distrnqg  6543  recmulnqg  6547  ltexnqq  6564  enq0tr  6590  distrnq0  6615  genpdflem  6663  distrlem1prl  6738  distrlem1pru  6739  muldivdirap  7758  divmuldivap  7763  prime  8396  eluz2  8575  raluz2  8618  elixx1  8867  elixx3g  8871  elioo2  8891  elioo5  8903  elicc4  8910  iccneg  8958  icoshft  8959  elfz1  8981  elfz  8982  elfz2  8983  elfzm11  9055  elfz2nn0  9075  elfzo2  9109  elfzo3  9121  lbfzo0  9139  fzind2  9197  zmodid2  9302  redivap  9702  imdivap  9709  findset  10457
  Copyright terms: Public domain W3C validator