Metamath Proof Explorer


Theorem ss2in

Description: Intersection of subclasses. (Contributed by NM, 5-May-2000)

Ref Expression
Assertion ss2in ABCDACBD

Proof

Step Hyp Ref Expression
1 ssrin ABACBC
2 sslin CDBCBD
3 1 2 sylan9ss ABCDACBD