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  8255  elznn0  8260  elznn  8261  zapne  8315  nn01to3  8552  elxr  8696
 Copyright terms: Public domain W3C validator