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 𝐴𝐵
ssini.2 𝐴𝐶
Assertion ssini 𝐴 ⊆ ( 𝐵𝐶 )

Proof

Step Hyp Ref Expression
1 ssini.1 𝐴𝐵
2 ssini.2 𝐴𝐶
3 1 2 pm3.2i ( 𝐴𝐵𝐴𝐶 )
4 ssin ( ( 𝐴𝐵𝐴𝐶 ) ↔ 𝐴 ⊆ ( 𝐵𝐶 ) )
5 3 4 mpbi 𝐴 ⊆ ( 𝐵𝐶 )