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