Syllogism is a tautology by phi16_

module Theorem where

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