Step | Hyp | Ref
| Expression |
1 | | 3dim0.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
2 | | 3dim0.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | 3dim0.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
4 | 1, 2, 3 | 3dim0 37949 |
. . 3
β’ (πΎ β HL β βπ‘ β π΄ βπ’ β π΄ βπ£ β π΄ βπ€ β π΄ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) |
5 | 4 | adantr 482 |
. 2
β’ ((πΎ β HL β§ π β π΄) β βπ‘ β π΄ βπ’ β π΄ βπ£ β π΄ βπ€ β π΄ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) |
6 | | simpl2 1193 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π = π‘) β (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄)) |
7 | 1, 2, 3 | 3dimlem1 37950 |
. . . . . . . . . . . 12
β’ (((π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)) β§ π = π‘) β (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) |
8 | 7 | 3ad2antl3 1188 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π = π‘) β (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) |
9 | 1, 2, 3 | 3dim1lem5 37958 |
. . . . . . . . . . 11
β’ (((π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
10 | 6, 8, 9 | syl2anc 585 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π = π‘) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
11 | | simp13 1206 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β π‘ β π΄) |
12 | | simp22 1208 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β π£ β π΄) |
13 | | simp23 1209 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β π€ β π΄) |
14 | 11, 12, 13 | 3jca 1129 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β (π‘ β π΄ β§ π£ β π΄ β§ π€ β π΄)) |
15 | 14 | ad2antrr 725 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π β π‘) β§ π β€ (π‘ β¨ π’)) β (π‘ β π΄ β§ π£ β π΄ β§ π€ β π΄)) |
16 | | simpll1 1213 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π β π‘) β§ π β€ (π‘ β¨ π’)) β (πΎ β HL β§ π β π΄ β§ π‘ β π΄)) |
17 | | simp21 1207 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β π’ β π΄) |
18 | | simp32 1211 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β Β¬ π£ β€ (π‘ β¨ π’)) |
19 | | simp33 1212 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)) |
20 | 17, 18, 19 | 3jca 1129 |
. . . . . . . . . . . . . 14
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β (π’ β π΄ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) |
21 | 20 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π β π‘) β§ π β€ (π‘ β¨ π’)) β (π’ β π΄ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) |
22 | | simplr 768 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π β π‘) β§ π β€ (π‘ β¨ π’)) β π β π‘) |
23 | | simpr 486 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π β π‘) β§ π β€ (π‘ β¨ π’)) β π β€ (π‘ β¨ π’)) |
24 | 1, 2, 3 | 3dimlem2 37951 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)) β§ (π β π‘ β§ π β€ (π‘ β¨ π’))) β (π β π‘ β§ Β¬ π£ β€ (π β¨ π‘) β§ Β¬ π€ β€ ((π β¨ π‘) β¨ π£))) |
25 | 16, 21, 22, 23, 24 | syl112anc 1375 |
. . . . . . . . . . . 12
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π β π‘) β§ π β€ (π‘ β¨ π’)) β (π β π‘ β§ Β¬ π£ β€ (π β¨ π‘) β§ Β¬ π€ β€ ((π β¨ π‘) β¨ π£))) |
26 | 1, 2, 3 | 3dim1lem5 37958 |
. . . . . . . . . . . 12
β’ (((π‘ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π‘ β§ Β¬ π£ β€ (π β¨ π‘) β§ Β¬ π€ β€ ((π β¨ π‘) β¨ π£))) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
27 | 15, 25, 26 | syl2anc 585 |
. . . . . . . . . . 11
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π β π‘) β§ π β€ (π‘ β¨ π’)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
28 | 11, 17, 13 | 3jca 1129 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β (π‘ β π΄ β§ π’ β π΄ β§ π€ β π΄)) |
29 | 28 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ π β€ ((π‘ β¨ π’) β¨ π£)) β (π‘ β π΄ β§ π’ β π΄ β§ π€ β π΄)) |
30 | | simp1 1137 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β (πΎ β HL β§ π β π΄ β§ π‘ β π΄)) |
31 | 17, 12 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β (π’ β π΄ β§ π£ β π΄)) |
32 | | simp31 1210 |
. . . . . . . . . . . . . . . . . 18
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β π‘ β π’) |
33 | 32, 19 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β (π‘ β π’ β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) |
34 | 30, 31, 33 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β ((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π‘ β π’ β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)))) |
35 | 34 | ad2antrr 725 |
. . . . . . . . . . . . . . 15
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ π β€ ((π‘ β¨ π’) β¨ π£)) β ((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π‘ β π’ β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)))) |
36 | | simplrl 776 |
. . . . . . . . . . . . . . 15
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ π β€ ((π‘ β¨ π’) β¨ π£)) β π β π‘) |
37 | | simplrr 777 |
. . . . . . . . . . . . . . 15
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ π β€ ((π‘ β¨ π’) β¨ π£)) β Β¬ π β€ (π‘ β¨ π’)) |
38 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ π β€ ((π‘ β¨ π’) β¨ π£)) β π β€ ((π‘ β¨ π’) β¨ π£)) |
39 | 1, 2, 3 | 3dimlem3 37953 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π‘ β π’ β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’) β§ π β€ ((π‘ β¨ π’) β¨ π£))) β (π β π‘ β§ Β¬ π’ β€ (π β¨ π‘) β§ Β¬ π€ β€ ((π β¨ π‘) β¨ π’))) |
40 | 35, 36, 37, 38, 39 | syl13anc 1373 |
. . . . . . . . . . . . . 14
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ π β€ ((π‘ β¨ π’) β¨ π£)) β (π β π‘ β§ Β¬ π’ β€ (π β¨ π‘) β§ Β¬ π€ β€ ((π β¨ π‘) β¨ π’))) |
41 | 1, 2, 3 | 3dim1lem5 37958 |
. . . . . . . . . . . . . 14
β’ (((π‘ β π΄ β§ π’ β π΄ β§ π€ β π΄) β§ (π β π‘ β§ Β¬ π’ β€ (π β¨ π‘) β§ Β¬ π€ β€ ((π β¨ π‘) β¨ π’))) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
42 | 29, 40, 41 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ π β€ ((π‘ β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
43 | 11, 17, 12 | 3jca 1129 |
. . . . . . . . . . . . . . 15
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β (π‘ β π΄ β§ π’ β π΄ β§ π£ β π΄)) |
44 | 43 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ Β¬ π β€ ((π‘ β¨ π’) β¨ π£)) β (π‘ β π΄ β§ π’ β π΄ β§ π£ β π΄)) |
45 | | simpl1 1192 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β (πΎ β HL β§ π β π΄ β§ π‘ β π΄)) |
46 | | simpl21 1252 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β π’ β π΄) |
47 | | simpl22 1253 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β π£ β π΄) |
48 | 46, 47 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β (π’ β π΄ β§ π£ β π΄)) |
49 | | simpl31 1255 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β π‘ β π’) |
50 | | simpl32 1256 |
. . . . . . . . . . . . . . . . . 18
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β Β¬ π£ β€ (π‘ β¨ π’)) |
51 | 49, 50 | jca 513 |
. . . . . . . . . . . . . . . . 17
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’))) |
52 | 45, 48, 51 | 3jca 1129 |
. . . . . . . . . . . . . . . 16
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β ((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’)))) |
53 | 52 | adantr 482 |
. . . . . . . . . . . . . . 15
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ Β¬ π β€ ((π‘ β¨ π’) β¨ π£)) β ((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’)))) |
54 | | simplr 768 |
. . . . . . . . . . . . . . 15
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ Β¬ π β€ ((π‘ β¨ π’) β¨ π£)) β (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) |
55 | | simpr 486 |
. . . . . . . . . . . . . . 15
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ Β¬ π β€ ((π‘ β¨ π’) β¨ π£)) β Β¬ π β€ ((π‘ β¨ π’) β¨ π£)) |
56 | 1, 2, 3 | 3dimlem4 37956 |
. . . . . . . . . . . . . . 15
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’)) β§ Β¬ π β€ ((π‘ β¨ π’) β¨ π£)) β (π β π‘ β§ Β¬ π’ β€ (π β¨ π‘) β§ Β¬ π£ β€ ((π β¨ π‘) β¨ π’))) |
57 | 53, 54, 55, 56 | syl3anc 1372 |
. . . . . . . . . . . . . 14
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ Β¬ π β€ ((π‘ β¨ π’) β¨ π£)) β (π β π‘ β§ Β¬ π’ β€ (π β¨ π‘) β§ Β¬ π£ β€ ((π β¨ π‘) β¨ π’))) |
58 | 1, 2, 3 | 3dim1lem5 37958 |
. . . . . . . . . . . . . 14
β’ (((π‘ β π΄ β§ π’ β π΄ β§ π£ β π΄) β§ (π β π‘ β§ Β¬ π’ β€ (π β¨ π‘) β§ Β¬ π£ β€ ((π β¨ π‘) β¨ π’))) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
59 | 44, 57, 58 | syl2anc 585 |
. . . . . . . . . . . . 13
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β§ Β¬ π β€ ((π‘ β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
60 | 42, 59 | pm2.61dan 812 |
. . . . . . . . . . . 12
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ (π β π‘ β§ Β¬ π β€ (π‘ β¨ π’))) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
61 | 60 | anassrs 469 |
. . . . . . . . . . 11
β’
(((((πΎ β HL
β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π β π‘) β§ Β¬ π β€ (π‘ β¨ π’)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
62 | 27, 61 | pm2.61dan 812 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β§ π β π‘) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
63 | 10, 62 | pm2.61dane 3033 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β§ (π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£))) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |
64 | 63 | 3exp 1120 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β ((π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β ((π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))))) |
65 | 64 | 3expd 1354 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π΄ β§ π‘ β π΄) β (π’ β π΄ β (π£ β π΄ β (π€ β π΄ β ((π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))))))) |
66 | 65 | 3exp 1120 |
. . . . . 6
β’ (πΎ β HL β (π β π΄ β (π‘ β π΄ β (π’ β π΄ β (π£ β π΄ β (π€ β π΄ β ((π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))))))))) |
67 | 66 | imp43 429 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄) β§ (π‘ β π΄ β§ π’ β π΄)) β (π£ β π΄ β (π€ β π΄ β ((π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)))))) |
68 | 67 | impd 412 |
. . . 4
β’ (((πΎ β HL β§ π β π΄) β§ (π‘ β π΄ β§ π’ β π΄)) β ((π£ β π΄ β§ π€ β π΄) β ((π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))))) |
69 | 68 | rexlimdvv 3205 |
. . 3
β’ (((πΎ β HL β§ π β π΄) β§ (π‘ β π΄ β§ π’ β π΄)) β (βπ£ β π΄ βπ€ β π΄ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)))) |
70 | 69 | rexlimdvva 3206 |
. 2
β’ ((πΎ β HL β§ π β π΄) β (βπ‘ β π΄ βπ’ β π΄ βπ£ β π΄ βπ€ β π΄ (π‘ β π’ β§ Β¬ π£ β€ (π‘ β¨ π’) β§ Β¬ π€ β€ ((π‘ β¨ π’) β¨ π£)) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)))) |
71 | 5, 70 | mpd 15 |
1
β’ ((πΎ β HL β§ π β π΄) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) |