Step | Hyp | Ref
| Expression |
1 | | simp11l 1285 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β πΎ β HL) |
2 | 1 | hllatd 37855 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β πΎ β Lat) |
3 | | simp12l 1287 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π β π΄) |
4 | | simp11 1204 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΎ β HL β§ π β π»)) |
5 | | simp21 1207 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΉ β π β§ πΊ β π)) |
6 | | cdlemg12.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
7 | | cdlemg12.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
8 | | cdlemg12.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
9 | | cdlemg12.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
10 | 6, 7, 8, 9 | ltrncoat 38636 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β (πΉβ(πΊβπ)) β π΄) |
11 | 4, 5, 3, 10 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΉβ(πΊβπ)) β π΄) |
12 | | eqid 2737 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
13 | | cdlemg12.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
14 | 12, 13, 7 | hlatjcl 37858 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβ(πΊβπ)) β π΄) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
15 | 1, 3, 11, 14 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
16 | | simp13l 1289 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π β π΄) |
17 | 6, 7, 8, 9 | ltrncoat 38636 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β (πΉβ(πΊβπ)) β π΄) |
18 | 4, 5, 16, 17 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΉβ(πΊβπ)) β π΄) |
19 | 12, 13, 7 | hlatjcl 37858 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβ(πΊβπ)) β π΄) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
20 | 1, 16, 18, 19 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) |
21 | | cdlemg12.m |
. . . 4
β’ β§ =
(meetβπΎ) |
22 | 12, 21 | latmcom 18359 |
. . 3
β’ ((πΎ β Lat β§ (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ) β§ (π β¨ (πΉβ(πΊβπ))) β (BaseβπΎ)) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) = ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ))))) |
23 | 2, 15, 20, 22 | syl3anc 1372 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) = ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ))))) |
24 | | cdlemg12b.r |
. . 3
β’ π
= ((trLβπΎ)βπ) |
25 | 6, 13, 21, 7, 8, 9,
24 | cdlemg19a 39175 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) |
26 | | simp13 1206 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
27 | | simp12 1205 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β π΄ β§ Β¬ π β€ π)) |
28 | | simp22 1208 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π β π) |
29 | 28 | necomd 3000 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β π β π) |
30 | | simp21r 1292 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β πΊ β π) |
31 | | simp23 1209 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβπ) β π) |
32 | 6, 7, 8, 9 | ltrnatneq 38674 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΊβπ) β π) β (πΊβπ) β π) |
33 | 4, 30, 27, 26, 31, 32 | syl131anc 1384 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (πΊβπ) β π) |
34 | | simp31 1210 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π
βπΊ) β€ (π β¨ π)) |
35 | 13, 7 | hlatjcom 37859 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) = (π β¨ π)) |
36 | 1, 3, 16, 35 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π β¨ π) = (π β¨ π)) |
37 | 34, 36 | breqtrd 5136 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β (π
βπΊ) β€ (π β¨ π)) |
38 | | simp32 1211 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π)) |
39 | 13, 7 | hlatjcom 37859 |
. . . . 5
β’ ((πΎ β HL β§ (πΉβ(πΊβπ)) β π΄ β§ (πΉβ(πΊβπ)) β π΄) β ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) = ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ)))) |
40 | 1, 11, 18, 39 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) = ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ)))) |
41 | 38, 40, 36 | 3netr3d 3021 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π)) |
42 | | simp33 1212 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) |
43 | | eqcom 2744 |
. . . . . 6
β’ ((π β¨ π) = (π β¨ π) β (π β¨ π) = (π β¨ π)) |
44 | 43 | anbi2i 624 |
. . . . 5
β’ ((Β¬
π β€ π β§ (π β¨ π) = (π β¨ π)) β (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) |
45 | 44 | rexbii 3098 |
. . . 4
β’
(βπ β
π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) |
46 | 42, 45 | sylnib 328 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π))) |
47 | 6, 13, 21, 7, 8, 9,
24 | cdlemg19a 39175 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) |
48 | 4, 26, 27, 5, 29, 33, 37, 41, 46, 47 | syl333anc 1403 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ (π β¨ (πΉβ(πΊβπ)))) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) |
49 | 23, 25, 48 | 3eqtr3d 2785 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉ β π β§ πΊ β π) β§ π β π β§ (πΊβπ) β π) β§ ((π
βπΊ) β€ (π β¨ π) β§ ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) β (π β¨ π) β§ Β¬ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β ((π β¨ (πΉβ(πΊβπ))) β§ π) = ((π β¨ (πΉβ(πΊβπ))) β§ π)) |