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

Theorem sylan9ssr 3523
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 3522 . 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 3481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-in 3488  df-ss 3495
This theorem is referenced by:  intssuni2  4313  marypha1  7906  cardinfima  8490  cfflb  8651  ssfin4  8702  acsfn  14931  mrelatlub  15690  efgval  16608  islbs3  17672  kgentopon  19907  txlly  20005  sigaclci  27957  mblfinlem3  29980  topjoin  30110  filnetlem3  30125  sspwimpALT  33206  sspwimpALT2  33209  bnj1014  33498
  Copyright terms: Public domain W3C validator