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

Theorem 3orass 927
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 925 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
2 orass 719 . 2 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2bitri 182 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wb 103  wo 664  w3o 923
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 665
This theorem depends on definitions:  df-bi 115  df-3or 925
This theorem is referenced by:  3orrot  930  3orcomb  933  3mix1  1112  sotritric  4142  sotritrieq  4143  ordtriexmid  4328  acexmidlemcase  5629  nntri3or  6236  nntri2  6237  elnnz  8730  elznn0  8735  elznn  8736  zapne  8791  nn01to3  9071  elxr  9216  bezoutlemmain  11080
  Copyright terms: Public domain W3C validator