Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > e002  Unicode version 
Description: A virtual deduction elimination rule. (Contributed by Alan Sare, 24Jun2011.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

e002.1  
e002.2  
e002.3  
e002.4 
Ref  Expression 

e002 
Step  Hyp  Ref  Expression 

1  e002.1  . . 3  
2  1  vd02 28675  . 2 
3  e002.2  . . 3  
4  3  vd02 28675  . 2 
5  e002.3  . 2  
6  e002.4  . 2  
7  2, 4, 5, 6  e222 28713  1 
Colors of variables: wff set class 
Syntax hints: wi 4 wvd2 28645 
This theorem was proved from axioms: ax1 5 ax2 6 ax3 7 axmp 8 
This theorem depends on definitions: dfbi 177 dfan 360 dfvd2 28646 
Copyright terms: Public domain  W3C validator 