diff --git a/tests/proofmode_clprop.ref b/tests/proofmode_clprop.ref
new file mode 100644
index 0000000000000000000000000000000000000000..e69de29bb2d1d6434b8b29ae775ad8c2e48c5391
diff --git a/tests/proofmode_clprop.v b/tests/proofmode_clprop.v
new file mode 100644
index 0000000000000000000000000000000000000000..3fab654f3676747d329cdcd0d1980cc37bbcd5b7
--- /dev/null
+++ b/tests/proofmode_clprop.v
@@ -0,0 +1,33 @@
+From iris.proofmode Require Import tactics.
+From iris.cl_logic Require Import bi.
+
+Section si_logic_tests.
+  Implicit Types P Q R : clProp.
+
+  Lemma test_everything_persistent P : P -∗ P.
+  Proof. by iIntros "#HP". Qed.
+
+  Lemma test_everything_affine P : P -∗ True.
+  Proof. by iIntros "_". Qed.
+
+  Lemma test_iIntro_impl P Q R : ⊢ P → Q ∧ R → P ∧ R.
+  Proof. iIntros "#HP #[HQ HR]". auto. Qed.
+
+  Lemma test_iApply_impl_1 P Q R : ⊢ P → (P → Q) → Q.
+  Proof. iIntros "HP HPQ". by iApply "HPQ". Qed.
+
+  Lemma test_iApply_impl_2 P Q R : ⊢ P → (P → Q) → Q.
+  Proof. iIntros "#HP #HPQ". by iApply "HPQ". Qed.
+
+  Lemma test_excluded_middle P Q : ⊢ P ∨ ¬P.
+  Proof.
+    iApply clProp.dn; iIntros "#H". iApply "H".
+    iRight. iIntros "HP". iApply "H". auto.
+  Qed.
+
+  Lemma test_peirces_law P Q : ((P → Q) → P) ⊢ P.
+  Proof.
+    iIntros "#H". iApply clProp.dn; iIntros "#HnotP". iApply "HnotP".
+    iApply "H". iIntros "HP". iDestruct ("HnotP" with "HP") as %[].
+  Qed.
+End si_logic_tests.