Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

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

pm5.12 
Step  Hyp  Ref  Expression 

1  pm2.51 156  . 2  
2  1  orri 377  1 
Colors of variables: wff setvar class 
Syntax hints: wn 3 wi 4 wo 369 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem depends on definitions: dfbi 188 dfor 371 
This theorem is referenced by: (None) 
Copyright terms: Public domain  W3C validator 