Syllogism is a tautology by chiguri

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 φ
syllogism-is-tauto P Q R φ | true  with ev Q φ
syllogism-is-tauto P Q R φ | true  | true  with ev R φ
syllogism-is-tauto P Q R φ | true  | true  | true  = refl
syllogism-is-tauto P Q R φ | true  | true  | false = refl
syllogism-is-tauto P Q R φ | true  | false with ev R φ
syllogism-is-tauto P Q R φ | true  | false | true  = refl
syllogism-is-tauto P Q R φ | true  | false | false = refl
syllogism-is-tauto P Q R φ | false with ev Q φ
syllogism-is-tauto P Q R φ | false | true  with ev R φ
syllogism-is-tauto P Q R φ | false | true  | true  = refl
syllogism-is-tauto P Q R φ | false | true  | false = refl
syllogism-is-tauto P Q R φ | false | false with ev R φ
syllogism-is-tauto P Q R φ | false | false | true  = refl
syllogism-is-tauto P Q R φ | false | false | false = refl