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

Theorem 3orass 948
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 946 . 2 ((𝜑𝜓𝜒) ↔ ((𝜑𝜓) ∨ 𝜒))
2 orass 739 . 2 (((𝜑𝜓) ∨ 𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
31, 2bitri 183 1 ((𝜑𝜓𝜒) ↔ (𝜑 ∨ (𝜓𝜒)))
Colors of variables: wff set class
Syntax hints:  wb 104  wo 680  w3o 944
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 681
This theorem depends on definitions:  df-bi 116  df-3or 946
This theorem is referenced by:  3orrot  951  3orcomb  954  3mix1  1133  sotritric  4206  sotritrieq  4207  ordtriexmid  4397  acexmidlemcase  5723  nntri3or  6343  nntri2  6344  elnnz  8968  elznn0  8973  elznn  8974  zapne  9029  nn01to3  9311  elxr  9456  bezoutlemmain  11532
  Copyright terms: Public domain W3C validator