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

Theorem sylan9ssr 3369
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 3368 . 2  |-  ( (
ph  /\  ps )  ->  A  C_  C )
43ancoms 453 1  |-  ( ( ps  /\  ph )  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    C_ wss 3327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3334  df-ss 3341
This theorem is referenced by:  intssuni2  4152  marypha1  7683  cardinfima  8266  cfflb  8427  ssfin4  8478  acsfn  14596  mrelatlub  15355  efgval  16213  islbs3  17235  kgentopon  19110  txlly  19208  sigaclci  26574  mblfinlem3  28428  topjoin  28584  filnetlem3  28599  sspwimpALT  31659  sspwimpALT2  31662  bnj1014  31951
  Copyright terms: Public domain W3C validator