MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sylan9ss Unicode version

Theorem sylan9ss 3192
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
StepHypRef Expression
1 sylan9ss.1 . 2  |-  ( ph  ->  A  C_  B )
2 sylan9ss.2 . 2  |-  ( ps 
->  B  C_  C )
3 sstr 3187 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2an 463 1  |-  ( (
ph  /\  ps )  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    C_ wss 3152
This theorem is referenced by:  sylan9ssr  3193  psstr  3280  unss12  3347  ss2in  3396  relrelss  5196  funssxp  5402  axdc3lem  8076  tskuni  8405  tsmsxp  17837  shslubi  21964  chlej12i  22054  rtrclreclem.min  24044  fnetr  26286  pcl0bN  30112
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator