Syllogism is a tautology by kdxu

module Theorem where
import Data.Bool
open import Definitions

syllogism-is-tauto : (P Q R : Form) -> tauto ((P ⊃ Q) ⊃ ((Q ⊃ R) ⊃ (P ⊃ R)))
syllogism-is-tauto p q r φ with ev p φ | ev q φ | ev r φ
syllogism-is-tauto p q r φ | Data.Bool.true | Data.Bool.true | Data.Bool.true = refl
syllogism-is-tauto p q r φ | Data.Bool.true | Data.Bool.true | Data.Bool.false = refl
syllogism-is-tauto p q r φ | Data.Bool.true | Data.Bool.false | Data.Bool.true = refl
syllogism-is-tauto p q r φ | Data.Bool.true | Data.Bool.false | Data.Bool.false = refl
syllogism-is-tauto p q r φ | Data.Bool.false | Data.Bool.true | Data.Bool.true = refl
syllogism-is-tauto p q r φ | Data.Bool.false | Data.Bool.true | Data.Bool.false = refl
syllogism-is-tauto p q r φ | Data.Bool.false | Data.Bool.false | Data.Bool.true = refl
syllogism-is-tauto p q r φ | Data.Bool.false | Data.Bool.false | Data.Bool.false = refl