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

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

Proof of Theorem 3orass
StepHypRef Expression
1 df-3or 897 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
2 orass 694 . 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:    <-> wb 102    \/ wo 639    \/ w3o 895
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 640
This theorem depends on definitions:  df-bi 114  df-3or 897
This theorem is referenced by:  3orrot  902  3orcomb  905  3mix1  1084  sotritric  4089  sotritrieq  4090  ordtriexmid  4275  acexmidlemcase  5535  nntri3or  6103  nntri2  6104  elnnz  8312  elznn0  8317  elznn  8318  zapne  8373  nn01to3  8649  elxr  8797
  Copyright terms: Public domain W3C validator