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

Metamath Proof Explorer

Theorem sylan9ss

Description: A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004) (Proof shortened by Andrew Salmon, 14-Jun-2011)

Ref Expression
Hypotheses sylan9ss.1 ⊢ φ → A ⊆ B
sylan9ss.2 ⊢ ψ → B ⊆ C
Assertion sylan9ss ⊢ φ ∧ ψ → A ⊆ C

Proof

Step Hyp Ref Expression
1 sylan9ss.1 ⊢ φ → A ⊆ B
2 sylan9ss.2 ⊢ ψ → B ⊆ C
3 sstr ⊢ A ⊆ B ∧ B ⊆ C → A ⊆ C
4 1 2 3 syl2an ⊢ φ ∧ ψ → A ⊆ C