Syllogism is a tautology by notogawa

module Theorem where

open import Definitions
open import Data.Bool

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 φ
... | true  | true  | true  = refl
... | true  | true  | false = refl
... | true  | false | true  = refl
... | true  | false | false = refl
... | false | true  | true  = refl
... | false | true  | false = refl
... | false | false | true  = refl
... | false | false | false = refl