Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > e00  Unicode version 
Description: Elimination rule identical to mp2 9. The nonvirtual deduction form is the virtual deduction form, which is mp2 9. (Contributed by Alan Sare, 14Jun2011.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

e00.1  
e00.2  
e00.3 
Ref  Expression 

e00 
Step  Hyp  Ref  Expression 

1  e00.1  . 2  
2  e00.2  . 2  
3  e00.3  . 2  
4  1, 2, 3  mp2 9  1 
Colors of variables: wff set class 
Syntax hints: wi 4 
This theorem is referenced by: 3impexpVD 28686 3impexpbicomVD 28687 onfrALTlem5VD 28715 
This theorem was proved from axioms: axmp 8 
Copyright terms: Public domain  W3C validator 