Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > pm5.31  Unicode version 
Description: Theorem *5.31 of [WhiteheadRussell] p. 125. (Contributed by NM, 3Jan2005.) 
Ref  Expression 

pm5.31 
Step  Hyp  Ref  Expression 

1  pm3.21 435  . . 3  
2  1  imim2d 48  . 2 
3  2  imp 418  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wa 358 
This theorem is referenced by: tartarmap 25888 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 177 dfan 360 
Copyright terms: Public domain  W3C validator 