blob: a47321054c054344cc39a9f1dd79a2f8d6508588 (
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
|
Theorem n3_47a : ∀ 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.
specialize Fact3_45 with P R Q.
intros Fact3_45a.
Syll Fact3_45a Simp3_26a Sa.
specialize n3_22 with R Q.
intros n3_22a.
specialize Syll2_05 with (P∧Q) (R∧Q) (Q∧R).
intros Syll2_05a. (*Not cited by Jorgensen*)
MP Syl2_05a n3_22a.
Syll Sa Syll2_05a Sb.
specialize Simp3_27 with (P→R) (Q→S).
intros Simp3_27a.
specialize Fact3_45 with Q S R.
intros Fact3_45b.
Syll Simp3_26a Fact3_45b Sc.
specialize n3_22 with S R.
intros n3_22b.
specialize Syll2_05 with (Q∧R) (S∧R) (R∧S).
intros Syll2_05b. (*Not cited by Jorgensen*)
MP Syl2_05b n3_22b.
Syll Sc Syll2_05a Sd.
specialize n2_83 with ((P→R)∧(Q→S)) (P∧Q) (Q∧R) (R∧S).
intros n2_83a. (*This with MP works, but it omits Conj3_03.*)
MP n2_83a Sb.
MP n2_83a Sd.
apply n2_83a.
Qed.
|
