Step | Hyp | Ref
| Expression |
1 | | simpl11 1249 |
. . . 4
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β πΎ β HL) |
2 | | simpl3l 1229 |
. . . 4
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β π β π΄) |
3 | | simpl3r 1230 |
. . . 4
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β π β π΄) |
4 | 1, 2, 3 | 3jca 1129 |
. . 3
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β (πΎ β HL β§ π β π΄ β§ π β π΄)) |
5 | | an6 1446 |
. . . . . 6
β’ (((π β π΄ β§ π β π΄ β§ π β π΄) β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β ((π β π΄ β§ π₯ β π) β§ (π β π΄ β§ π¦ β π) β§ (π β π΄ β§ π§ β π))) |
6 | | ssel2 3940 |
. . . . . . 7
β’ ((π β π΄ β§ π₯ β π) β π₯ β π΄) |
7 | | ssel2 3940 |
. . . . . . 7
β’ ((π β π΄ β§ π¦ β π) β π¦ β π΄) |
8 | | ssel2 3940 |
. . . . . . 7
β’ ((π β π΄ β§ π§ β π) β π§ β π΄) |
9 | 6, 7, 8 | 3anim123i 1152 |
. . . . . 6
β’ (((π β π΄ β§ π₯ β π) β§ (π β π΄ β§ π¦ β π) β§ (π β π΄ β§ π§ β π)) β (π₯ β π΄ β§ π¦ β π΄ β§ π§ β π΄)) |
10 | 5, 9 | sylbi 216 |
. . . . 5
β’ (((π β π΄ β§ π β π΄ β§ π β π΄) β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯ β π΄ β§ π¦ β π΄ β§ π§ β π΄)) |
11 | 10 | 3ad2antl2 1187 |
. . . 4
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ (π₯ β π β§ π¦ β π β§ π§ β π)) β (π₯ β π΄ β§ π¦ β π΄ β§ π§ β π΄)) |
12 | 11 | adantrr 716 |
. . 3
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β (π₯ β π΄ β§ π¦ β π΄ β§ π§ β π΄)) |
13 | | simpl12 1250 |
. . . 4
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β π β π§) |
14 | | simpl13 1251 |
. . . 4
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β π₯ β π¦) |
15 | | simprr1 1222 |
. . . 4
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β Β¬ π β€ (π₯ β¨ π¦)) |
16 | 13, 14, 15 | 3jca 1129 |
. . 3
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β (π β π§ β§ π₯ β π¦ β§ Β¬ π β€ (π₯ β¨ π¦))) |
17 | | simprr2 1223 |
. . 3
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β π β€ (π₯ β¨ π)) |
18 | | simprr3 1224 |
. . 3
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β π β€ (π¦ β¨ π§)) |
19 | | paddasslem.l |
. . . 4
β’ β€ =
(leβπΎ) |
20 | | paddasslem.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
21 | | paddasslem.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
22 | 19, 20, 21 | paddasslem4 38332 |
. . 3
β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π₯ β π΄ β§ π¦ β π΄ β§ π§ β π΄) β§ (π β π§ β§ π₯ β π¦ β§ Β¬ π β€ (π₯ β¨ π¦))) β§ (π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§))) β βπ β π΄ (π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§))) |
23 | 4, 12, 16, 17, 18, 22 | syl32anc 1379 |
. 2
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β βπ β π΄ (π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§))) |
24 | | simpl2 1193 |
. . . . 5
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β (π β π΄ β§ π β π΄ β§ π β π΄)) |
25 | | simpl3 1194 |
. . . . 5
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β (π β π΄ β§ π β π΄)) |
26 | 1, 24, 25 | 3jca 1129 |
. . . 4
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β (πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄))) |
27 | 26 | adantr 482 |
. . 3
β’
(((((πΎ β HL
β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β§ (π β π΄ β§ (π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§)))) β (πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄))) |
28 | | simplrl 776 |
. . 3
β’
(((((πΎ β HL
β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β§ (π β π΄ β§ (π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§)))) β (π₯ β π β§ π¦ β π β§ π§ β π)) |
29 | 15, 18 | jca 513 |
. . . 4
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π¦ β¨ π§))) |
30 | 29 | adantr 482 |
. . 3
β’
(((((πΎ β HL
β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β§ (π β π΄ β§ (π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§)))) β (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π¦ β¨ π§))) |
31 | | simprl 770 |
. . . 4
β’
(((((πΎ β HL
β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β§ (π β π΄ β§ (π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§)))) β π β π΄) |
32 | | simprrl 780 |
. . . 4
β’
(((((πΎ β HL
β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β§ (π β π΄ β§ (π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§)))) β π β€ (π₯ β¨ π¦)) |
33 | | simprrr 781 |
. . . 4
β’
(((((πΎ β HL
β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β§ (π β π΄ β§ (π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§)))) β π β€ (π β¨ π§)) |
34 | 31, 32, 33 | 3jca 1129 |
. . 3
β’
(((((πΎ β HL
β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β§ (π β π΄ β§ (π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§)))) β (π β π΄ β§ π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§))) |
35 | | paddasslem.p |
. . . 4
β’ + =
(+πβπΎ) |
36 | 19, 20, 21, 35 | paddasslem9 38337 |
. . 3
β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π¦ β¨ π§)) β§ (π β π΄ β§ π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§)))) β π β ((π + π) + π)) |
37 | 27, 28, 30, 34, 36 | syl13anc 1373 |
. 2
β’
(((((πΎ β HL
β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β§ (π β π΄ β§ (π β€ (π₯ β¨ π¦) β§ π β€ (π β¨ π§)))) β π β ((π + π) + π)) |
38 | 23, 37 | rexlimddv 3155 |
1
β’ ((((πΎ β HL β§ π β π§ β§ π₯ β π¦) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((π₯ β π β§ π¦ β π β§ π§ β π) β§ (Β¬ π β€ (π₯ β¨ π¦) β§ π β€ (π₯ β¨ π) β§ π β€ (π¦ β¨ π§)))) β π β ((π + π) + π)) |