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

Theorem syl5sseqr 3227
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl5sseqr.1  |-  B  C_  A
syl5sseqr.2  |-  ( ph  ->  C  =  A )
Assertion
Ref Expression
syl5sseqr  |-  ( ph  ->  B  C_  C )

Proof of Theorem syl5sseqr
StepHypRef Expression
1 syl5sseqr.1 . . 3  |-  B  C_  A
21a1i 10 . 2  |-  ( ph  ->  B  C_  A )
3 syl5sseqr.2 . 2  |-  ( ph  ->  C  =  A )
42, 3sseqtr4d 3215 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    C_ wss 3152
This theorem is referenced by:  unissint  3886  resdif  5494  fimacnv  5657  domss2  7020  dffi3  7184  cantnfp1lem3  7382  trcl  7410  tcid  7424  r1ordg  7450  r1sssuc  7455  ackbij1lem15  7860  cfsmolem  7896  isfin4-3  7941  fin1a2lem7  8032  wunex2  8360  wuncid  8365  fsumsplit  12212  o1fsum  12271  incexclem  12295  incexc  12296  phimullem  12847  vdwlem6  13033  ressinbas  13204  mrcssid  13519  mreexexlem2d  13547  acsfiindd  14280  dirge  14359  efgredlemf  15050  efgredlemd  15053  gsumzres  15194  gsumzcl  15195  gsumzf1o  15196  gsumzaddlem  15203  gsumadd  15205  gsumzsplit  15206  gsumsplit2  15208  gsumconst  15209  gsumzoppg  15216  dprd2da  15277  dmdprdsplit2lem  15280  dmdprdsplit2  15281  dmdprdsplit  15282  dprdsplit  15283  invrpropd  15480  issubdrg  15570  lspssid  15742  aspssid  16073  pjcss  16616  istopon  16663  sscls  16793  ordtbas  16922  cncls2  17002  tgcmp  17128  cmpfi  17135  1stcfb  17171  1stckgenlem  17248  ptbasfi  17276  ptcnplem  17315  ptuncnv  17498  ptunhmeo  17499  fbasrn  17579  cnflf2  17698  fclscmp  17725  alexsublem  17738  ghmcnp  17797  tsmsgsum  17821  tsmsres  17826  tsmssplit  17834  tsmsxplem1  17835  mopnfss  17989  cnmpt2pc  18426  uniiccdif  18933  uniioombllem3  18940  uniioombllem4  18941  itg2splitlem  19103  itg2split  19104  itgsplit  19190  ellimc2  19227  ellimc3  19229  lhop  19363  plyaddlem1  19595  plymullem1  19596  taylthlem2  19753  mtest  19781  xrlimcnp  20263  fsumharmonic  20305  chtdif  20396  dchrghm  20495  lgsquadlem2  20594  dchrisumlema  20637  dchrisumlem2  20639  dchrisum0lem1b  20664  dchrisum0lem1  20665  pntrlog2bndlem6  20732  pntlemf  20754  ex-res  20828  spanss2  21924  mdsymi  22991  cvmliftlem10  23825  rtrclreclem.refl  24041  rnintintrn  25126  segray  26155  heibor1lem  26533  heibor  26545  divrngcl  26588  isdrngo2  26589  igenss  26687  nacsfix  26787  isnumbasgrplem2  27269  rgspnssid  27375  paddunssN  29997  sspadd1  30004  sspadd2  30005  pclssidN  30084  diassdvaN  31250  dochvalr  31547  lcdvbase  31783
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator