Mathbox for Jeff Hankins 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > exp5d  Structured version Unicode version 
Description: An exportation inference. (Contributed by Jeff Hankins, 7Jul2009.) 
Ref  Expression 

exp5d.1 
Ref  Expression 

exp5d 
Step  Hyp  Ref  Expression 

1  exp5d.1  . . 3  
2  1  expd 434  . 2 
3  2  exp31 602  1 
Colors of variables: wff setvar class 
Syntax hints: wi 4 wa 367 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 ax3 8 
This theorem depends on definitions: dfbi 185 dfan 369 
This theorem is referenced by: exp56 30366 
Copyright terms: Public domain  W3C validator 