blob: e1c51b880a9dfa7b8fd55f4c5767511815597468 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
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.
|
