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

Metamath Proof Explorer

Theorem psssstrd

Description: Transitivity involving subclass and proper subclass inclusion. Deduction form of psssstr . (Contributed by David Moews, 1-May-2017)

Ref Expression
Hypotheses psssstrd.1 ⊢ φ → A ⊂ B
psssstrd.2 ⊢ φ → B ⊆ C
Assertion psssstrd ⊢ φ → A ⊂ C

Proof

Step Hyp Ref Expression
1 psssstrd.1 ⊢ φ → A ⊂ B
2 psssstrd.2 ⊢ φ → B ⊆ C
3 psssstr ⊢ A ⊂ B ∧ B ⊆ C → A ⊂ C
4 1 2 3 syl2anc ⊢ φ → A ⊂ C