Syllogism is a tautology by Rotsor

module Theorem where

open import Definitions
open import Data.Bool

_⇒_ : Bool → Bool → Bool
x ⇒ y = not x ∨ y

sit : ∀ P Q R → ((P ⇒ Q) ⇒ ((Q ⇒ R) ⇒ (P ⇒ R))) == true
sit true true true = refl
sit true true false = refl
sit true false R = refl
sit false true true = refl
sit false true false = refl
sit false false R = refl

syllogism-is-tauto : (P Q R : Form) -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)))
syllogism-is-tauto p q r c = sit (ev p c) (ev q c) (ev r c)