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 ⊢ A ⊆ B
ssini.2 ⊢ A ⊆ C
Assertion ssini ⊢ A ⊆ B ∩ C

Proof

Step Hyp Ref Expression
1 ssini.1 ⊢ A ⊆ B
2 ssini.2 ⊢ A ⊆ C
3 1 2 pm3.2i ⊢ A ⊆ B ∧ A ⊆ C
4 ssin ⊢ A ⊆ B ∧ A ⊆ C ↔ A ⊆ B ∩ C
5 3 4 mpbi ⊢ A ⊆ B ∩ C