diff --git a/ClassicalLogic/ClassicalFive.agda b/ClassicalLogic/ClassicalFive.agda
new file mode 100644
index 0000000..d963ae9
--- /dev/null
+++ b/ClassicalLogic/ClassicalFive.agda
@@ -0,0 +1,46 @@
+{-# OPTIONS --safe --warning=error --without-K #-}
+
+open import LogicalFormulae
+
+open import Agda.Primitive using (Level; lzero; lsuc; _⊔_)
+
+module ClassicalLogic.ClassicalFive where
+
+em = {A : Set} → (A || (A → False))
+dne = {A : Set} → ((A → False) → False) → A
+peirce = {A B : Set} → ((A → B) → A) → A
+iad = {A B : Set} → (A → B) → ((A → False) || B)
+
+emToDne : em → dne
+emToDne em {A} pr with em {A}
+emToDne em {A} pr | inl x = x
+emToDne em {A} pr | inr x = exFalso (pr x)
+
+dneToPeirce : dne → peirce
+dneToPeirce dne {A} {B} aba = dne (λ z → z (aba (λ z₁ → dne (λ _ → z z₁))))
+
+peirceToIad : peirce → iad
+peirceToIad peirce {A} {B} aToB = peirce (λ z → inl (λ x → z (inr (aToB x))))
+
+iadToEm : iad → em
+iadToEm iad {A} with (iad {A} {A} (λ i → i))
+iadToEm iad {A} | inl x = inr x
+iadToEm iad {A} | inr x = inl x
+
+dem = {A B : Set} → (((A → False) && (B → False)) → False) → A || B
+
+demToEm : dem → em
+demToEm dem {A} = dem (λ z → _&&_.snd z (_&&_.fst z))
+
+emToDem : em → dem
+emToDem em {A} {B} pr with em {A}
+emToDem em {A} {B} pr | inl x = inl x
+emToDem em {A} {B} pr | inr x with em {B}
+emToDem em {A} {B} pr | inr x | inl x₁ = inr x₁
+emToDem em {A} {B} pr | inr x | inr y = exFalso (pr (x ,, y))
+
+isContr : {a : _} (A : Set a) → Set a
+isContr T = (x y : T) → x ≡ y
+
+pr : {a : _} {A : Set a} → {x : A} → isContr (Sg A (λ y → x ≡ y))
+pr {A = A} {.a} (a , refl) (.a , refl) = refl