Step | Hyp | Ref
| Expression |
1 | | ssltex1 27524 |
. . 3
âĒ (ðī <<s ðķ â ðī â V) |
2 | 1 | 3ad2ant3 1133 |
. 2
âĒ ((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â ðī â V) |
3 | | simp1 1134 |
. 2
âĒ ((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â ðĩ â ðŦ No
) |
4 | | ssltss1 27526 |
. . 3
âĒ (ðī <<s ðķ â ðī â No
) |
5 | 4 | 3ad2ant3 1133 |
. 2
âĒ ((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â ðī â No
) |
6 | 3 | elpwid 4610 |
. 2
âĒ ((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â ðĩ â No
) |
7 | | breq2 5151 |
. . . . . 6
âĒ (ðĨ = ð â (ðĶ âĪs ðĨ â ðĶ âĪs ð)) |
8 | 7 | rexbidv 3176 |
. . . . 5
âĒ (ðĨ = ð â (âðĶ â ðķ ðĶ âĪs ðĨ â âðĶ â ðķ ðĶ âĪs ð)) |
9 | | simp12 1202 |
. . . . 5
âĒ (((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ) |
10 | | simp3 1136 |
. . . . 5
âĒ (((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â ð â ðĩ) |
11 | 8, 9, 10 | rspcdva 3612 |
. . . 4
âĒ (((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â âðĶ â ðķ ðĶ âĪs ð) |
12 | | breq1 5150 |
. . . . 5
âĒ (ðĶ = ð â (ðĶ âĪs ð â ð âĪs ð)) |
13 | 12 | cbvrexvw 3233 |
. . . 4
âĒ
(âðĶ â
ðķ ðĶ âĪs ð â âð â ðķ ð âĪs ð) |
14 | 11, 13 | sylib 217 |
. . 3
âĒ (((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â âð â ðķ ð âĪs ð) |
15 | | simpl13 1248 |
. . . . . 6
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ðī <<s ðķ) |
16 | 15, 4 | syl 17 |
. . . . 5
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ðī â No
) |
17 | | simpl2 1190 |
. . . . 5
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ð â ðī) |
18 | 16, 17 | sseldd 3982 |
. . . 4
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ð â No
) |
19 | | ssltss2 27527 |
. . . . . 6
âĒ (ðī <<s ðķ â ðķ â No
) |
20 | 15, 19 | syl 17 |
. . . . 5
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ðķ â No
) |
21 | | simprl 767 |
. . . . 5
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ð â ðķ) |
22 | 20, 21 | sseldd 3982 |
. . . 4
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ð â No
) |
23 | | simpl1 1189 |
. . . . . 6
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â (ðĩ â ðŦ No
â§ âðĨ
â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ)) |
24 | 23, 6 | syl 17 |
. . . . 5
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ðĩ â No
) |
25 | | simpl3 1191 |
. . . . 5
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ð â ðĩ) |
26 | 24, 25 | sseldd 3982 |
. . . 4
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ð â No
) |
27 | 15, 17, 21 | ssltsepcd 27532 |
. . . 4
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ð <s ð) |
28 | | simprr 769 |
. . . 4
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ð âĪs ð) |
29 | 18, 22, 26, 27, 28 | sltletrd 27499 |
. . 3
âĒ ((((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â§ (ð â ðķ â§ ð âĪs ð)) â ð <s ð) |
30 | 14, 29 | rexlimddv 3159 |
. 2
âĒ (((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â§ ð â ðī â§ ð â ðĩ) â ð <s ð) |
31 | 2, 3, 5, 6, 30 | ssltd 27529 |
1
âĒ ((ðĩ â ðŦ No â§ âðĨ â ðĩ âðĶ â ðķ ðĶ âĪs ðĨ â§ ðī <<s ðķ) â ðī <<s ðĩ) |