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

Metamath Proof Explorer

Theorem sylan9ssr

Description: A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004)

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

Proof

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