Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > e00  Structured version 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 29042 3impexpbicomVD 29043 onfrALTlem5VD 29071 
This theorem was proved from axioms: axmp 5 
Copyright terms: Public domain  W3C validator 