Many changes to PL.v file, proved PM axiomsHEADmaster

1 files changed, 39 insertions, 0 deletions

diff --git a/Yuelin.v b/Yuelin.v
new file mode 100644
index 0000000..e1c51b8
--- /dev/null
+++ b/Yuelin.v
@@ -0,0 +1,39 @@
+Import No1.

+Import No2.

+Import No3.

+Import No4.

+Import No5. 

+

+ Theorem n3_47 : ∀ P Q R S : Prop,

+ ((P → R) ∧ (Q → S)) → (P ∧ Q) → R ∧ S.

+Proof. intros P Q R S.

+ specialize Simp3_26 with (P→R) (Q→S).

+ intros Simp3_26a. (*Yuelin's book has n2_34. This doesn't exist.*)

+ specialize Fact3_45 with P R Q.

+ intros Fact3_45a. (*Yuelin's book has n2_45. Fact3_45 is meant.*)

+ replace (R∧Q) with (Q∧R) in Fact3_45a.

+ Syll Simp3_26a Fact3_45a Sa. (*Syll2_05*)

+ specialize Simp3_27 with (P→R) (Q→S).

+ intros Simp3_27a. (*Yuelin's book has n2_36. This doesn't exist.*)

+ specialize Fact3_45 with Q S R.

+ intros Fact3_45b. (*Yuelin's book has n2_45. Fact3_45 is meant.*)

+ replace (S∧R) with (R∧S) in Fact3_45b.

+ Syll Simp3_27a Fact3_45b Sb. (*Syll2_05*)

+ clear Simp3_26a. clear Fact3_45a. 

+   clear Simp3_27a. clear Fact3_45b.

+ Conj Sa Sb.

+ split.

+ apply Sa.

+ apply Sb.

+ specialize Comp3_43 with ((P→R)∧(Q→S)) ((P∧Q)→(Q∧R)) ((Q∧R)→(R∧S)).

+ intros Comp3_43a. (*Yuelin's book has n2_39. Comp3_43 is meant. PM and I have n2_83 here.*)

+ MP Comp3_43a H.

+ specialize Syll3_33 with (P∧Q) (Q∧R) (R∧S).

+ intros Syll3_33a. (*Yuelin's book has n2_39. Syll3_33 is meant. My n2_83 does this work, too.*)

+ Syll Comp3_43a Syll3_33a Sc. (*Yuelin seems to do another application of Syll3_33, citing the same number n2_39. But that would also require here, as above, Conjunction, which Yuelin does not bother citing.*)

+ apply Sc.

+ apply EqBi.

+ apply n4_3.

+ apply EqBi.

+ apply n4_3.

+Qed.
\ No newline at end of file