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 451 1  |-  ( ( ps  /\  ph )  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  intssuni2  4297  marypha1  7886  cardinfima  8469  cfflb  8630  ssfin4  8681  acsfn  15148  mrelatlub  16015  efgval  16934  islbs3  17996  kgentopon  20205  txlly  20303  sigaclci  28362  mblfinlem3  30293  topjoin  30423  filnetlem3  30438  sspwimpALT  34126  sspwimpALT2  34129  bnj1014  34419
  Copyright terms: Public domain W3C validator