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

Theorem df3nandALT1 26146
 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 414 . . 3
2 imnan 412 . . . . . . . 8
32biimpi 187 . . . . . . 7
43, 3jca 519 . . . . . 6
52biimpri 198 . . . . . . 7
65adantl 453 . . . . . 6
74, 6impbii 181 . . . . 5
8 df-nan 1297 . . . . . 6
98, 8anbi12i 679 . . . . 5
107, 9bitr4i 244 . . . 4
1110imbi2i 304 . . 3
12 df-nan 1297 . . . . 5
1312anbi2i 676 . . . 4
1413notbii 288 . . 3
151, 11, 143bitr4i 269 . 2
16 df-3nand 26145 . 2
17 df-nan 1297 . 2
1815, 16, 173bitr4i 269 1
 Colors of variables: wff set class Syntax hints:   wn 3   wi 4   wb 177   wa 359   wnan 1296   w3nand 26144 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 178  df-an 361  df-nan 1297  df-3nand 26145
 Copyright terms: Public domain W3C validator