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

Theorem 3orass 981
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 979 . 2  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ( ph  \/  ps )  \/  ch ) )
2 orass 767 . 2  |-  ( ( ( ph  \/  ps )  \/  ch )  <->  (
ph  \/  ( ps  \/  ch ) ) )
31, 2bitri 184 1  |-  ( (
ph  \/  ps  \/  ch )  <->  ( ph  \/  ( ps  \/  ch ) ) )
Colors of variables: wff set class
Syntax hints:    <-> wb 105    \/ wo 708    \/ w3o 977
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 709
This theorem depends on definitions:  df-bi 117  df-3or 979
This theorem is referenced by:  3orrot  984  3orcomb  987  3mix1  1166  sotritric  4324  sotritrieq  4325  ordtriexmid  4520  ontriexmidim  4521  acexmidlemcase  5869  nntri3or  6493  nntri2  6494  exmidontriimlem1  7219  elnnz  9261  elznn0  9266  elznn  9267  zapne  9325  nn01to3  9615  elxr  9774  bezoutlemmain  11993  lgsdilem  14321
  Copyright terms: Public domain W3C validator