Description: An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eelTTT.1 | |
|
eelTTT.2 | |
||
eelTTT.3 | |
||
eelTTT.4 | |
||
Assertion | eelTTT | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eelTTT.1 | |
|
2 | eelTTT.2 | |
|
3 | eelTTT.3 | |
|
4 | eelTTT.4 | |
|
5 | truan | |
|
6 | 3anass | |
|
7 | truan | |
|
8 | 6 7 | bitri | |
9 | 1 4 | syl3an1 | |
10 | 8 9 | sylbir | |
11 | 2 10 | sylan | |
12 | 5 11 | sylbir | |
13 | 3 12 | syl | |
14 | 13 | mptru | |