diff options
| author | Landon D. C. Elkind | 2021-04-20 14:25:04 -0600 |
|---|---|---|
| committer | GitHub | 2021-04-20 14:25:04 -0600 |
| commit | b8bb530a36cae219e6951152d378ca5d13fa2f3e (patch) | |
| tree | f84b5f81c1ab48efd7489f73a2a010155bf57bb7 /Lemma5_7.v | |
| parent | e1fa90fe793e67af9e8a70ef8db4b8fc42b331ee (diff) | |
Diffstat (limited to 'Lemma5_7.v')
| -rw-r--r-- | Lemma5_7.v | 39 |
1 files changed, 39 insertions, 0 deletions
diff --git a/Lemma5_7.v b/Lemma5_7.v new file mode 100644 index 0000000..ff600cd --- /dev/null +++ b/Lemma5_7.v @@ -0,0 +1,39 @@ +Theorem L5_7 : ∀ P Q R S : Prop,
+ ((P↔Q) ∧ (R↔S)) → ((P↔R) → (Q↔S)).
+Proof. intros P Q R S.
+ specialize n4_22 with Q P R.
+ intros n4_22a.
+ specialize n4_22 with Q R S.
+ intros n4_22b.
+ specialize Exp3_3 with (Q↔R) (R↔S) (Q↔S).
+ intros Exp3_3a.
+ MP Exp3_3a n4_22b.
+ Syll n4_22a Exp3_3a Sa.
+ replace (Q↔P) with (P↔Q) in Sa.
+ specialize Imp3_31 with ((P↔Q)∧(P↔R)) (R↔S) (Q↔S).
+ intros Imp3_31a.
+ MP Imp3_31a Sa.
+ replace (((P ↔ Q) ∧ (P ↔ R)) ∧ (R ↔ S)) with
+ ((P ↔ Q) ∧((P ↔ R) ∧ (R ↔ S))) in Imp3_31a.
+ replace ((P ↔ R) ∧ (R ↔ S)) with
+ ((R ↔ S) ∧ (P ↔ R)) in Imp3_31a.
+ replace ((P ↔ Q) ∧ (R ↔ S) ∧ (P ↔ R)) with
+ (((P ↔ Q) ∧ (R ↔ S)) ∧ (P ↔ R)) in Imp3_31a.
+ specialize Exp3_3 with ((P ↔ Q) ∧ (R ↔ S)) (P↔R) (Q↔S).
+ intros Exp3_3b.
+ MP Exp3_3b Imp3_31a.
+ apply Exp3_3b.
+ apply EqBi.
+ apply n4_32. (*With (P ↔ Q) (R ↔ S) (P ↔ R)*)
+ apply EqBi.
+ apply n4_3. (*With (R ↔ S) (P ↔ R)*)
+ replace ((P ↔ Q) ∧((P ↔ R) ∧ (R ↔ S))) with
+ (((P ↔ Q) ∧ (P ↔ R)) ∧ (R ↔ S)).
+ reflexivity.
+ apply EqBi.
+ specialize n4_32 with (P↔Q) (P↔R) (R↔S).
+ intros n4_32a.
+ apply n4_32a.
+ apply EqBi.
+ apply n4_21. (*With P Q*)
+Qed.
\ No newline at end of file |