Description: Deduction of abstraction subclass from implication. (Contributed by NM, 29-Jul-2011) (Revised by Steven Nguyen, 28-Jun-2024)
Ref | Expression | ||
---|---|---|---|
Hypothesis | ss2abdv.1 | ||
Assertion | ss2abdv |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ss2abdv.1 | ||
2 | 1 | sbimdv | |
3 | df-clab | ||
4 | df-clab | ||
5 | 2 3 4 | 3imtr4g | |
6 | 5 | ssrdv |