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

Theorem 3orass 950
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 948 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
2 orass 741 . 2  |-  ( ( ( ph  \/  ps )  \/  ch )  <->  (
ph  \/  ( ps  \/  ch ) ) )
31, 2bitri 183 1  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 104    \/ wo 682    \/ w3o 946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 683
This theorem depends on definitions:  df-bi 116  df-3or 948
This theorem is referenced by:  3orrot  953  3orcomb  956  3mix1  1135  sotritric  4216  sotritrieq  4217  ordtriexmid  4407  acexmidlemcase  5737  nntri3or  6357  nntri2  6358  elnnz  9022  elznn0  9027  elznn  9028  zapne  9083  nn01to3  9365  elxr  9518  bezoutlemmain  11598
  Copyright terms: Public domain W3C validator