blob: d32a0969de8a97b3816b67f7860d5fda2d0e2bab (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
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.
|
