diff options
Diffstat (limited to 'Jorgensen3_47.v')
| -rw-r--r-- | Jorgensen3_47.v | 31 |
1 files changed, 31 insertions, 0 deletions
diff --git a/Jorgensen3_47.v b/Jorgensen3_47.v new file mode 100644 index 0000000..a473210 --- /dev/null +++ b/Jorgensen3_47.v @@ -0,0 +1,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.
\ No newline at end of file |