1 files changed, 19 insertions, 0 deletions
diff --git a/Nicod1_4.v b/Nicod1_4.v
new file mode 100644
index 0000000..d32a096
--- /dev/null
+++ b/Nicod1_4.v
@@ -0,0 +1,19 @@
+Theorem N1_4 : ∀ P Q : Prop,
+  P ∨ Q → Q ∨ P.
+Proof. intros P Q.
+  specialize n2_2 with Q P.
+  intros n2_2a.
+  specialize Assoc1_5 with P Q P.
+  intros Assoc1_5a.
+  specialize Sum1_6 with P Q (Q ∨ P).
+  intros Sum1_6a.
+  MP Sum1_6a n2_2a.
+  Syll Sum1_6a Assoc1_5a Sa.
+  specialize Taut1_2 with P.
+  intros Taut1_2a.
+  specialize Sum1_6 with Q (P ∨ P) P.
+  intros Sum1_6b.
+  MP Sum1_6b Taut1_2a.
+  Syll Sa Sum1_6b Sb.
+  apply Sb.
+Qed.
+\ No newline at end of file