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

Theorem syl5sseqr 3393
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 11 . 2  |-  ( ph  ->  B  C_  A )
3 syl5sseqr.2 . 2  |-  ( ph  ->  C  =  A )
42, 3sseqtr4d 3381 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1362    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-an 371  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-in 3323  df-ss 3330
This theorem is referenced by:  unissint  4140  resdif  5649  fimacnv  5823  tfrlem5  6825  domss2  7458  dffi3  7669  cantnfp1lem3  7876  cantnfp1lem3OLD  7902  trcl  7936  tcid  7947  r1ordg  7973  r1sssuc  7978  ackbij1lem15  8391  cfsmolem  8427  isfin4-3  8472  fin1a2lem7  8563  wunex2  8893  wuncid  8898  fsumsplit  13200  o1fsum  13259  phimullem  13837  vdwlem6  14030  ressinbas  14217  mrcssid  14538  mreexexlem2d  14566  acsfiindd  15330  dirge  15390  symgbasfi  15871  efgredlemf  16218  efgredlemd  16221  gsumzres  16368  gsumzcl2  16369  gsumzf1o  16371  gsumzresOLD  16372  gsumzclOLD  16373  gsumzf1oOLD  16374  gsumzaddlemOLD  16390  gsumadd  16392  gsumaddOLD  16393  gsumzsplit  16398  gsumzsplitOLD  16399  gsumsplit2  16402  gsumsplit2OLD  16403  gsumzoppgOLD  16417  dprd2da  16515  dmdprdsplit2lem  16518  dmdprdsplit2  16519  dmdprdsplit  16520  dprdsplit  16521  invrpropd  16724  issubdrg  16814  lspssid  16988  aspssid  17326  pjcss  17983  istopon  18372  sscls  18502  ordtbas  18638  cncls2  18719  tgcmp  18846  cmpfi  18853  1stcfb  18891  1stckgenlem  18968  ptbasfi  18996  ptcnplem  19036  ptuncnv  19222  ptunhmeo  19223  fbasrn  19299  cnflf2  19418  fclscmp  19445  alexsublem  19458  ghmcnp  19527  tsmsgsum  19551  tsmsgsumOLD  19554  tsmsresOLD  19559  tsmsres  19560  tsmssplit  19568  tsmsxplem1  19569  ustssco  19631  mopnfss  19860  cnmpt2pc  20342  uniiccdif  20900  uniioombllem3  20907  uniioombllem4  20908  itg2splitlem  21068  itg2split  21069  itgsplit  21155  ellimc2  21194  ellimc3  21196  lhop  21330  plyaddlem1  21566  plymullem1  21567  taylthlem2  21724  mtest  21754  xrlimcnp  22247  fsumharmonic  22290  chtdif  22381  dchrghm  22480  lgsquadlem2  22579  dchrisumlema  22622  dchrisumlem2  22624  dchrisum0lem1b  22649  dchrisum0lem1  22650  pntrlog2bndlem6  22717  pntlemf  22739  ex-res  23471  spanss2  24571  mdsymi  25638  ordtconlem1  26208  issgon  26420  sssigagen  26442  measiuns  26485  cvmliftlem10  27031  rtrclreclem.refl  27193  fprodsplit  27323  ftc1anclem6  28316  heibor1lem  28552  heibor  28564  divrngcl  28607  isdrngo2  28608  igenss  28706  nacsfix  28893  isnumbasgrplem2  29305  rgspnssid  29372  itgpowd  29435  paddunssN  33025  sspadd1  33032  sspadd2  33033  pclssidN  33112  diassdvaN  34278  dochvalr  34575  lcdvbase  34811
  Copyright terms: Public domain W3C validator