Metamath Proof Explorer

Theorem ssind

Description: A deduction showing that a subclass of two classes is a subclass of their intersection. (Contributed by Jonathan Ben-Naim, 3-Jun-2011)

Ref Expression
Hypotheses ssind.1 φ A B
ssind.2 φ A C
Assertion ssind φ A B C


Step Hyp Ref Expression
1 ssind.1 φ A B
2 ssind.2 φ A C
3 1 2 jca φ A B A C
4 ssin A B A C A B C
5 3 4 sylib φ A B C