This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 ⊆ ( 𝐵 ∩ 𝐶 )