Description: Generalization of elimhyps that is not useful unless we can separately prove |- A e. _V . (Contributed by NM, 13-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypothesis | elimhyps2.1 | |
|
Assertion | elimhyps2 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elimhyps2.1 | |
|
2 | dfsbcq | |
|
3 | dfsbcq | |
|
4 | 2 3 1 | elimhyp | |