Metamath Proof Explorer


Theorem inss

Description: Inclusion of an intersection of two classes. (Contributed by NM, 30-Oct-2014)

Ref Expression
Assertion inss ACBCABC

Proof

Step Hyp Ref Expression
1 ssinss1 ACABC
2 incom AB=BA
3 ssinss1 BCBAC
4 2 3 eqsstrid BCABC
5 1 4 jaoi ACBCABC