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

Metamath Proof Explorer

Theorem psstrd

Description: Proper subclass inclusion is transitive. Deduction form of psstr . (Contributed by David Moews, 1-May-2017)

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

Proof

Step Hyp Ref Expression
1 psstrd.1 ⊢ φ → A ⊂ B
2 psstrd.2 ⊢ φ → B ⊂ C
3 psstr ⊢ A ⊂ B ∧ B ⊂ C → A ⊂ C
4 1 2 3 syl2anc ⊢ φ → A ⊂ C