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

Theorem 3orass 888
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 886 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
2 orass 684 . 2 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2bitri 173 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wb 98  wo 629  w3o 884
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 630
This theorem depends on definitions:  df-bi 110  df-3or 886
This theorem is referenced by:  3orrot  891  3orcomb  894  3mix1  1073  sotritric  4061  sotritrieq  4062  ordtriexmid  4247  acexmidlemcase  5507  nntri3or  6072  nntri2  6073  elnnz  8253  elznn0  8258  elznn  8259  zapne  8313  nn01to3  8550  elxr  8694
  Copyright terms: Public domain W3C validator