Theorem sylan9ss 3616

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

Hypotheses

Ref	Expression
sylan9ss.1	|- ( ph -> A C_ B )
sylan9ss.2	|- ( ps -> B C_ C )

Assertion

Ref	Expression
sylan9ss	|- ( ( ph /\ ps ) -> A C_ C )

Proof of Theorem sylan9ss

Step	Hyp	Ref	Expression
1		sylan9ss.1	. 2 |- ( ph -> A C_ B )
2		sylan9ss.2	. 2 |- ( ps -> B C_ C )
3		sstr 3611	. 2 |- ( ( A C_ B /\ B C_ C ) -> A C_ C )
4	1, 2, 3	syl2an 494	1 |- ( ( ph /\ ps ) -> A C_ C )

Syntax hints:   -> wi 4   /\ wa 384   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-in 3581  df-ss 3588

This theorem is referenced by:  sylan9ssr  3617  psstr  3711  unss12  3785  ss2in  3840  ssdisj  4026  relrelss  5659  funssxp  6061  axdc3lem  9272  tskuni  9605  rtrclreclem4  13801  tsmsxp  21958  shslubi  28244  chlej12i  28334  insiga  30200  fnetr  32346  pcl0bN  35209  brtrclfv2  38019