Syllogism is a tautology by strout

module Theorem where

open import Data.Bool renaming(true to t;false to f)
open import Definitions

x : ∀ P Q R -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)))
x P Q R φ with ev P φ | ev Q φ | ev R φ
... | t | t | t = refl
... | t | t | f = refl
... | t | f | r = refl
... | f | t | t = refl
... | f | t | f = refl
... | f | f | r = refl

syllogism-is-tauto = x