Metamath Proof Explorer


Theorem sylan9ssr

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

Ref Expression
Hypotheses sylan9ssr.1 φAB
sylan9ssr.2 ψBC
Assertion sylan9ssr ψφAC

Proof

Step Hyp Ref Expression
1 sylan9ssr.1 φAB
2 sylan9ssr.2 ψBC
3 1 2 sylan9ss φψAC
4 3 ancoms ψφAC