diff options
| author | Landon D. C. Elkind | 2021-04-20 14:25:04 -0600 |
|---|---|---|
| committer | GitHub | 2021-04-20 14:25:04 -0600 |
| commit | b8bb530a36cae219e6951152d378ca5d13fa2f3e (patch) | |
| tree | f84b5f81c1ab48efd7489f73a2a010155bf57bb7 /Nicod1_4.v | |
| parent | e1fa90fe793e67af9e8a70ef8db4b8fc42b331ee (diff) | |
Diffstat (limited to 'Nicod1_4.v')
| -rw-r--r-- | Nicod1_4.v | 19 |
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 |