Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > nicdfim  Unicode version 
Description: Define implication in terms of 'nand'. Analogous to . In a pure (standalone) treatment of Nicod's axiom, this theorem would be changed to a definition ($a statement). (Contributed by NM, 11Dec2008.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

nicdfim 
Step  Hyp  Ref  Expression 

1  nanim 1297  . . 3  
2  1  bicomi 195  . 2 
3  nanbi 1299  . 2  
4  2, 3  mpbi 201  1 
Colors of variables: wff set class 
Syntax hints: wi 6 wb 178 wnan 1292 
This theorem is referenced by: nicstdmp 1450 nicluk1 1451 nicluk2 1452 nicluk3 1453 
This theorem was proved from axioms: ax1 7 ax2 8 ax3 9 axmp 10 
This theorem depends on definitions: dfbi 179 dfor 361 dfan 362 dfnan 1293 
Copyright terms: Public domain  W3C validator 