Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π β§ Β¬ π
β€ (π β¨ π))) β πΎ β HL) |
2 | | simp21 1207 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π β§ Β¬ π
β€ (π β¨ π))) β π β π΄) |
3 | | simp23 1209 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π β§ Β¬ π
β€ (π β¨ π))) β π
β π΄) |
4 | | simp21 1207 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β π β π΄) |
5 | | simp23 1209 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β π
β π΄) |
6 | | simp22 1208 |
. . . . . . . 8
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β π β π΄) |
7 | 4, 5, 6 | 3jca 1129 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β (π β π΄ β§ π
β π΄ β§ π β π΄)) |
8 | | 2lnne.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
9 | | 2lnne.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
10 | | 2lnne.a |
. . . . . . . 8
β’ π΄ = (AtomsβπΎ) |
11 | 8, 9, 10 | hlatexch2 37905 |
. . . . . . 7
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄ β§ π β π΄) β§ π β π) β (π β€ (π
β¨ π) β π
β€ (π β¨ π))) |
12 | 7, 11 | syld3an2 1412 |
. . . . . 6
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β (π β€ (π
β¨ π) β π
β€ (π β¨ π))) |
13 | 12 | con3d 152 |
. . . . 5
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ π β π) β (Β¬ π
β€ (π β¨ π) β Β¬ π β€ (π
β¨ π))) |
14 | 13 | 3exp 1120 |
. . . 4
β’ (πΎ β HL β ((π β π΄ β§ π β π΄ β§ π
β π΄) β (π β π β (Β¬ π
β€ (π β¨ π) β Β¬ π β€ (π
β¨ π))))) |
15 | 14 | imp4a 424 |
. . 3
β’ (πΎ β HL β ((π β π΄ β§ π β π΄ β§ π
β π΄) β ((π β π β§ Β¬ π
β€ (π β¨ π)) β Β¬ π β€ (π
β¨ π)))) |
16 | 15 | 3imp 1112 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π β§ Β¬ π
β€ (π β¨ π))) β Β¬ π β€ (π
β¨ π)) |
17 | 8, 9, 10 | 2llnne2N 37917 |
. 2
β’ ((πΎ β HL β§ (π β π΄ β§ π
β π΄) β§ Β¬ π β€ (π
β¨ π)) β (π
β¨ π) β (π
β¨ π)) |
18 | 1, 2, 3, 16, 17 | syl121anc 1376 |
1
β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π β§ Β¬ π
β€ (π β¨ π))) β (π
β¨ π) β (π
β¨ π)) |