Description: An inference showing that a subclass of two classes is a subclass of their intersection. (Contributed by NM, 24-Nov-2003)
Ref | Expression | ||
---|---|---|---|
Hypotheses | ssini.1 | |
|
ssini.2 | |
||
Assertion | ssini | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ssini.1 | |
|
2 | ssini.2 | |
|
3 | 1 2 | pm3.2i | |
4 | ssin | |
|
5 | 3 4 | mpbi | |