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

Theorem sylan9ss 3517
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 3512 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2an 477 1  |-  ( (
ph  /\  ps )  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3483  df-ss 3490
This theorem is referenced by:  sylan9ssr  3518  psstr  3608  unss12  3676  ss2in  3725  relrelss  5529  funssxp  5742  axdc3lem  8826  tskuni  9157  tsmsxp  20392  shslubi  25979  chlej12i  26069  insiga  27777  rtrclreclem.min  28545  fnetr  29758  pcl0bN  34719
  Copyright terms: Public domain W3C validator