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

Theorem 3orass 887
Description: Associative law for triple disjunction. (Contributed by NM, 8-Apr-1994.)
Assertion
Ref Expression
3orass ((φ ψ χ) ↔ (φ (ψ χ)))

Proof of Theorem 3orass
StepHypRef Expression
1 df-3or 885 . 2 ((φ ψ χ) ↔ ((φ ψ) χ))
2 orass 683 . 2 (((φ ψ) χ) ↔ (φ (ψ χ)))
31, 2bitri 173 1 ((φ ψ χ) ↔ (φ (ψ χ)))
Colors of variables: wff set class
Syntax hints:  wb 98   wo 628   w3o 883
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 629
This theorem depends on definitions:  df-bi 110  df-3or 885
This theorem is referenced by:  3orrot  890  3orcomb  893  3mix1  1072  sotritric  4052  sotritrieq  4053  ordtriexmid  4210  acexmidlemcase  5450  nntri3or  6011  nntri2  6012  elnnz  8011  elznn0  8016  elznn  8017  zapne  8071  nn01to3  8308  elxr  8446
  Copyright terms: Public domain W3C validator