Description: An elimination deduction. (Contributed by Alan Sare, 4-Feb-2017) (Proof modification is discouraged.) (New usage is discouraged.)
Ref | Expression | ||
---|---|---|---|
Hypotheses | eelT00.1 | |- ( T. -> ph ) |
|
eelT00.2 | |- ps |
||
eelT00.3 | |- ch |
||
eelT00.4 | |- ( ( ph /\ ps /\ ch ) -> th ) |
||
Assertion | eelT00 | |- th |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eelT00.1 | |- ( T. -> ph ) |
|
2 | eelT00.2 | |- ps |
|
3 | eelT00.3 | |- ch |
|
4 | eelT00.4 | |- ( ( ph /\ ps /\ ch ) -> th ) |
|
5 | 3anass | |- ( ( T. /\ ps /\ ch ) <-> ( T. /\ ( ps /\ ch ) ) ) |
|
6 | truan | |- ( ( T. /\ ( ps /\ ch ) ) <-> ( ps /\ ch ) ) |
|
7 | 5 6 | bitri | |- ( ( T. /\ ps /\ ch ) <-> ( ps /\ ch ) ) |
8 | 1 4 | syl3an1 | |- ( ( T. /\ ps /\ ch ) -> th ) |
9 | 7 8 | sylbir | |- ( ( ps /\ ch ) -> th ) |
10 | 2 9 | mpan | |- ( ch -> th ) |
11 | 3 10 | ax-mp | |- th |