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

Theorem 3orass 966
 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 964 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
2 orass 757 . 2 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2bitri 183 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
 Colors of variables: wff set class Syntax hints:   ↔ wb 104   ∨ wo 698   ∨ w3o 962 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699 This theorem depends on definitions:  df-bi 116  df-3or 964 This theorem is referenced by:  3orrot  969  3orcomb  972  3mix1  1151  sotritric  4255  sotritrieq  4256  ordtriexmid  4446  acexmidlemcase  5779  nntri3or  6399  nntri2  6400  elnnz  9111  elznn0  9116  elznn  9117  zapne  9172  nn01to3  9459  elxr  9616  bezoutlemmain  11745
 Copyright terms: Public domain W3C validator