Metamath Proof Explorer 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > pm4.66  Unicode version 
Description: Theorem *4.66 of [WhiteheadRussell] p. 120. (Contributed by NM, 3Jan2005.) 
Ref  Expression 

pm4.66 
Step  Hyp  Ref  Expression 

1  pm4.64 363  1 
Colors of variables: wff set class 
Syntax hints: wn 5 wi 6 wb 178 wo 359 
This theorem is referenced by: pm4.54 481 hirstLax3 27149 
This theorem was proved from axioms: ax1 7 ax2 8 ax3 9 axmp 10 
This theorem depends on definitions: dfbi 179 dfor 361 
Copyright terms: Public domain  W3C validator 