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

Theorem sylan9ssr 3503
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 3502 . 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 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:  intssuni2  4297  marypha1  7896  cardinfima  8481  cfflb  8642  ssfin4  8693  acsfn  14933  mrelatlub  15690  efgval  16609  islbs3  17675  kgentopon  19912  txlly  20010  sigaclci  28005  mblfinlem3  30028  topjoin  30158  filnetlem3  30173  sspwimpALT  33453  sspwimpALT2  33456  bnj1014  33746
  Copyright terms: Public domain W3C validator