Step | Hyp | Ref
| Expression |
1 | | simp1 1137 |
. 2
âĒ ((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) â ðī â ðŦ No
) |
2 | | ssltex2 27130 |
. . 3
âĒ (ðĩ <<s ðķ â ðķ â V) |
3 | 2 | 3ad2ant3 1136 |
. 2
âĒ ((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) â ðķ â V) |
4 | 1 | elpwid 4570 |
. 2
âĒ ((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) â ðī â No
) |
5 | | ssltss2 27132 |
. . 3
âĒ (ðĩ <<s ðķ â ðķ â No
) |
6 | 5 | 3ad2ant3 1136 |
. 2
âĒ ((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) â ðķ â No
) |
7 | | breq1 5109 |
. . . . . 6
âĒ (ðĨ = ð â (ðĨ âĪs ðĶ â ð âĪs ðĶ)) |
8 | 7 | rexbidv 3176 |
. . . . 5
âĒ (ðĨ = ð â (âðĶ â ðĩ ðĨ âĪs ðĶ â âðĶ â ðĩ ð âĪs ðĶ)) |
9 | | simp12 1205 |
. . . . 5
âĒ (((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) â âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ) |
10 | | simp2 1138 |
. . . . 5
âĒ (((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) â ð â ðī) |
11 | 8, 9, 10 | rspcdva 3583 |
. . . 4
âĒ (((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) â âðĶ â ðĩ ð âĪs ðĶ) |
12 | | breq2 5110 |
. . . . 5
âĒ (ðĶ = ð â (ð âĪs ðĶ â ð âĪs ð)) |
13 | 12 | cbvrexvw 3227 |
. . . 4
âĒ
(âðĶ â
ðĩ ð âĪs ðĶ â âð â ðĩ ð âĪs ð) |
14 | 11, 13 | sylib 217 |
. . 3
âĒ (((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) â âð â ðĩ ð âĪs ð) |
15 | | simpl11 1249 |
. . . . . 6
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ðī â ðŦ No
) |
16 | 15 | elpwid 4570 |
. . . . 5
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ðī â No
) |
17 | | simpl2 1193 |
. . . . 5
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ð â ðī) |
18 | 16, 17 | sseldd 3946 |
. . . 4
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ð â No
) |
19 | | simpl13 1251 |
. . . . . 6
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ðĩ <<s ðķ) |
20 | | ssltss1 27131 |
. . . . . 6
âĒ (ðĩ <<s ðķ â ðĩ â No
) |
21 | 19, 20 | syl 17 |
. . . . 5
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ðĩ â No
) |
22 | | simprl 770 |
. . . . 5
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ð â ðĩ) |
23 | 21, 22 | sseldd 3946 |
. . . 4
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ð â No
) |
24 | 19, 5 | syl 17 |
. . . . 5
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ðķ â No
) |
25 | | simpl3 1194 |
. . . . 5
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ð â ðķ) |
26 | 24, 25 | sseldd 3946 |
. . . 4
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ð â No
) |
27 | | simprr 772 |
. . . 4
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ð âĪs ð) |
28 | 19, 22, 25 | ssltsepcd 27136 |
. . . 4
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ð <s ð) |
29 | 18, 23, 26, 27, 28 | slelttrd 27112 |
. . 3
âĒ ((((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) ⧠(ð â ðĩ ⧠ð âĪs ð)) â ð <s ð) |
30 | 14, 29 | rexlimddv 3159 |
. 2
âĒ (((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) ⧠ð â ðī ⧠ð â ðķ) â ð <s ð) |
31 | 1, 3, 4, 6, 30 | ssltd 27134 |
1
âĒ ((ðī â ðŦ No ⧠âðĨ â ðī âðĶ â ðĩ ðĨ âĪs ðĶ ⧠ðĩ <<s ðķ) â ðī <<s ðķ) |