Description: A version of elimhyp using explicit substitution. (Contributed by NM, 15-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | elimhyps.1 | |
|
Assertion | elimhyps | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elimhyps.1 | |
|
2 | sbceq1a | |
|
3 | dfsbcq | |
|
4 | 2 3 1 | elimhyp | |