blob: ff600cd17979fbc2544c07e2b209ada55cae9131 (
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
|
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.
|
