Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > nicbijust  Unicode version 
Description: For nic* definitions, the biconditional connective is not used. Instead, definitions are made based on this form. nicbi1 1443 and nicbi2 1444 are used to convert the definitions into usable theorems about one side of the implication. (Contributed by Jeff Hoffman, 18Nov2007.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

nicbijust 
Step  Hyp  Ref  Expression 

1  nicswap 1434  1 
Colors of variables: wff set class 
Syntax hints: wnan 1287 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 177 dfan 360 dfnan 1288 
Copyright terms: Public domain  W3C validator 