Mathbox for Alan Sare 
< Previous
Next >
Nearby theorems 

Mirrors > Home > MPE Home > Th. List > Mathboxes > ee100  Structured version Unicode version 
Description: e100 33611 without virtual deductions. (Contributed by Alan Sare, 23Jul2011.) (Proof modification is discouraged.) (New usage is discouraged.) 
Ref  Expression 

ee100.1  
ee100.2  
ee100.3  
ee100.4 
Ref  Expression 

ee100 
Step  Hyp  Ref  Expression 

1  ee100.1  . 2  
2  ee100.2  . . 3  
3  2  a1i 11  . 2 
4  ee100.3  . . 3  
5  4  a1i 11  . 2 
6  ee100.4  . 2  
7  1, 3, 5, 6  syl3c 61  1 
Colors of variables: wff setvar class 
Syntax hints: wi 4 
This theorem was proved from axioms: axmp 5 ax1 6 ax2 7 
This theorem is referenced by: (None) 
Copyright terms: Public domain  W3C validator 