Step | Hyp | Ref
| Expression |
1 | | simp3r 1203 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β (πΉβπ) = π) |
2 | | simpl1 1192 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β§ Β¬ π β€ π) β (πΎ β HL β§ π β π»)) |
3 | | simpl21 1252 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β§ Β¬ π β€ π) β πΉ β π) |
4 | | simpl22 1253 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β§ Β¬ π β€ π) β (π β π΄ β§ Β¬ π β€ π)) |
5 | | simpl23 1254 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β§ Β¬ π β€ π) β π β π΄) |
6 | | simpr 486 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β§ Β¬ π β€ π) β Β¬ π β€ π) |
7 | 5, 6 | jca 513 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β§ Β¬ π β€ π) β (π β π΄ β§ Β¬ π β€ π)) |
8 | | simpl3l 1229 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β§ Β¬ π β€ π) β (πΉβπ) β π) |
9 | | ltrn2eq.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
10 | | ltrn2eq.a |
. . . . . 6
β’ π΄ = (AtomsβπΎ) |
11 | | ltrn2eq.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
12 | | ltrn2eq.t |
. . . . . 6
β’ π = ((LTrnβπΎ)βπ) |
13 | 9, 10, 11, 12 | ltrnatneq 38648 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β (πΉβπ) β π) |
14 | 2, 3, 4, 7, 8, 13 | syl131anc 1384 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β§ Β¬ π β€ π) β (πΉβπ) β π) |
15 | 14 | ex 414 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β (Β¬ π β€ π β (πΉβπ) β π)) |
16 | 15 | necon4bd 2964 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β ((πΉβπ) = π β π β€ π)) |
17 | 1, 16 | mpd 15 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β π β€ π) |