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

Theorem sylan9ss 3477
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 3472 . 2  |-  ( ( A  C_  B  /\  B  C_  C )  ->  A  C_  C )
41, 2, 3syl2an 479 1  |-  ( (
ph  /\  ps )  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 370    C_ wss 3436
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2408  df-cleq 2414  df-clel 2417  df-in 3443  df-ss 3450
This theorem is referenced by:  sylan9ssr  3478  psstr  3569  unss12  3638  ss2in  3689  relrelss  5375  funssxp  5756  axdc3lem  8881  tskuni  9209  rtrclreclem4  13113  tsmsxp  21156  shslubi  27024  chlej12i  27114  insiga  28955  fnetr  31000  pcl0bN  33407  brtrclfv2  36179
  Copyright terms: Public domain W3C validator