Mathbox for Anthony Hart < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df3nandALT1 Structured version   Unicode version

Theorem df3nandALT1 31062
 Description: The double nand expressed in terms of pure nand. (Contributed by Anthony Hart, 2-Sep-2011.)
Assertion
Ref Expression
df3nandALT1

Proof of Theorem df3nandALT1
StepHypRef Expression
1 iman 425 . . 3
2 imnan 423 . . . . . . . 8
32biimpi 197 . . . . . . 7
43, 3jca 534 . . . . . 6
52biimpri 209 . . . . . . 7
65adantl 467 . . . . . 6
74, 6impbii 190 . . . . 5
8 df-nan 1380 . . . . . 6
98, 8anbi12i 701 . . . . 5
107, 9bitr4i 255 . . . 4
1110imbi2i 313 . . 3
12 df-nan 1380 . . . . 5
1312anbi2i 698 . . . 4
1413notbii 297 . . 3
151, 11, 143bitr4i 280 . 2
16 df-3nand 31061 . 2
17 df-nan 1380 . 2
1815, 16, 173bitr4i 280 1
 Colors of variables: wff setvar class Syntax hints:   wn 3   wi 4   wb 187   wa 370   wnan 1379   w3nand 31060 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 188  df-an 372  df-nan 1380  df-3nand 31061 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator