Metamath Proof Explorer


Theorem ssini

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
|- A C_ B
ssini.2
|- A C_ C
Assertion ssini
|- A C_ ( B i^i C )

Proof

Step Hyp Ref Expression
1 ssini.1
 |-  A C_ B
2 ssini.2
 |-  A C_ C
3 1 2 pm3.2i
 |-  ( A C_ B /\ A C_ C )
4 ssin
 |-  ( ( A C_ B /\ A C_ C ) <-> A C_ ( B i^i C ) )
5 3 4 mpbi
 |-  A C_ ( B i^i C )