Description: An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eel000cT.1 | |- ph |
|
eel000cT.2 | |- ps |
||
eel000cT.3 | |- ch |
||
eel000cT.4 | |- ( ( ph /\ ps /\ ch ) -> th ) |
||
Assertion | eel000cT | |- ( T. -> th ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eel000cT.1 | |- ph |
|
2 | eel000cT.2 | |- ps |
|
3 | eel000cT.3 | |- ch |
|
4 | eel000cT.4 | |- ( ( ph /\ ps /\ ch ) -> th ) |
|
5 | 1 4 | mp3an1 | |- ( ( ps /\ ch ) -> th ) |
6 | 2 5 | mpan | |- ( ch -> th ) |
7 | 3 6 | ax-mp | |- th |
8 | 7 | a1i | |- ( T. -> th ) |