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 1301  . . 3  
2  1  bicomi 194  . 2 
3  nanbi 1303  . 2  
4  2, 3  mpbi 200  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wb 177 wnan 1296 
This theorem is referenced by: nicstdmp 1464 nicluk1 1465 nicluk2 1466 nicluk3 1467 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 178 dfor 360 dfan 361 dfnan 1297 
Copyright terms: Public domain  W3C validator 