Table of ContentsRelated theorems
Unicode version
| Table of Contents |
Mathbox for Anthony Hart |
< Previous
Next >
Related theorems Unicode version |
| Description: The double nand expressed in terms of pure nand. |
| Ref | Expression |
|---|---|
| df3nandALT1 |
        |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | iman 256 |
. . 3
 
 | |
| 2 | imnan 261 |
. . . . . . . 8
| |
| 3 | 2 | biimpi 168 |
. . . . . . 7
|
| 4 | 3, 3 | jca 310 |
. . . . . 6
|
| 5 | 2 | biimpri 169 |
. . . . . . 7
|
| 6 | 5 | adantl 424 |
. . . . . 6
|
| 7 | 4, 6 | impbii 174 |
. . . . 5
|
| 8 | df-nand 1230 |
. . . . . 6
| |
| 9 | 8, 8 | anbi12i 540 |
. . . . 5
|
| 10 | 7, 9 | bitr4i 193 |
. . . 4
|
| 11 | 10 | imbi2i 202 |
. . 3
|
| 12 | df-nand 1230 |
. . . . 5
| |
| 13 | 12 | anbi2i 538 |
. . . 4
|
| 14 | 13 | notbii 204 |
. . 3
|
| 15 | 1, 11, 14 | 3bitr4i 200 |
. 2
|
| 16 | df-3nand 14145 |
. 2
| |
| 17 | df-nand 1230 |
. 2
| |
| 18 | 15, 16, 17 | 3bitr4i 200 |
1
|
| Colors of variables: wff set class |
| Syntax hints: wn 2
wi 3
wb 163
wa 240
wnand 1229 w3nand 14144 |
| This theorem was proved from axioms: ax-1 4 ax-2 5 ax-3 6 ax-mp 7 |
| This theorem depends on definitions: df-bi 164 df-an 242 df-nand 1230 df-3nand 14145 |