Metamath Proof Explorer


Theorem ssinss1d

Description: Intersection preserves subclass relationship. (Contributed by Glauco Siliprandi, 17-Aug-2020)

Ref Expression
Hypothesis ssinss1d.1
|- ( ph -> A C_ C )
Assertion ssinss1d
|- ( ph -> ( A i^i B ) C_ C )

Proof

Step Hyp Ref Expression
1 ssinss1d.1
 |-  ( ph -> A C_ C )
2 ssinss1
 |-  ( A C_ C -> ( A i^i B ) C_ C )
3 1 2 syl
 |-  ( ph -> ( A i^i B ) C_ C )