Syllogism is a tautology by masahiro_sakai

module Theorem where

open import Definitions
open import Data.Bool

f : (P Q R : Bool) → (not (not P ∨ Q) ∨ (not (not Q ∨ R) ∨ (not P ∨ R))) == true
f false false false = refl
f false false true = refl
f false true false = refl
f false true true = refl
f true false false = refl
f true false true = refl
f true true false = refl
f true true true = refl

syllogism-is-tauto : (P Q R : Form) -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)))
syllogism-is-tauto P Q R φ = f (ev P φ) (ev Q φ) (ev R φ)