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

Theorem sylan9ss 3502
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 3497 . 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 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  sylan9ssr  3503  psstr  3593  unss12  3661  ss2in  3710  relrelss  5521  funssxp  5734  axdc3lem  8833  tskuni  9164  tsmsxp  20635  shslubi  26281  chlej12i  26371  insiga  28115  rtrclreclem.min  29048  fnetr  30145  pcl0bN  35522
  Copyright terms: Public domain W3C validator