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

Theorem 3orass 923
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 921 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
2 orass 717 . 2 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2bitri 182 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wb 103  wo 662  w3o 919
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 663
This theorem depends on definitions:  df-bi 115  df-3or 921
This theorem is referenced by:  3orrot  926  3orcomb  929  3mix1  1108  sotritric  4087  sotritrieq  4088  ordtriexmid  4273  acexmidlemcase  5538  nntri3or  6137  nntri2  6138  elnnz  8442  elznn0  8447  elznn  8448  zapne  8503  nn01to3  8783  elxr  8928  bezoutlemmain  10531
  Copyright terms: Public domain W3C validator