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

Theorem sylan9ssr 3279
Description: A subclass transitivity deduction. (Contributed by NM, 27-Sep-2004.)
Hypotheses
Ref Expression
sylan9ssr.1  |-  ( ph  ->  A  C_  B )
sylan9ssr.2  |-  ( ps 
->  B  C_  C )
Assertion
Ref Expression
sylan9ssr  |-  ( ( ps  /\  ph )  ->  A  C_  C )

Proof of Theorem sylan9ssr
StepHypRef Expression
1 sylan9ssr.1 . . 3  |-  ( ph  ->  A  C_  B )
2 sylan9ssr.2 . . 3  |-  ( ps 
->  B  C_  C )
31, 2sylan9ss 3278 . 2  |-  ( (
ph  /\  ps )  ->  A  C_  C )
43ancoms 439 1  |-  ( ( ps  /\  ph )  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358    C_ wss 3238
This theorem is referenced by:  intssuni2  3989  marypha1  7334  cardinfima  7871  cfflb  8032  ssfin4  8083  acsfn  13771  mrelatlub  14499  efgval  15236  islbs3  16118  kgentopon  17450  txlly  17547  topjoin  25821  filnetlem3  25836  sspwimpALT  28465  bnj1014  28756
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1551  ax-5 1562  ax-17 1621  ax-9 1659  ax-8 1680  ax-6 1734  ax-7 1739  ax-11 1751  ax-12 1937  ax-ext 2347
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1324  df-ex 1547  df-nf 1550  df-sb 1654  df-clab 2353  df-cleq 2359  df-clel 2362  df-in 3245  df-ss 3252
  Copyright terms: Public domain W3C validator