Description: el2122old without virtual deductions. (Contributed by Alan Sare, 13-Jun-2015) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eel2122old.1 | ||
eel2122old.2 | |||
eel2122old.3 | |||
eel2122old.4 | |||
Assertion | eel2122old |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eel2122old.1 | ||
2 | eel2122old.2 | ||
3 | eel2122old.3 | ||
4 | eel2122old.4 | ||
5 | 4 | 3exp | |
6 | 1 5 | syl | |
7 | 2 6 | syl5 | |
8 | 3 7 | syl7 | |
9 | 8 | ex | |
10 | 9 | pm2.43d | |
11 | 10 | pm2.43d | |
12 | 11 | imp |