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

Theorem syl5sseqr 3466
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 3454 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1399    C_ wss 3389
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-clab 2368  df-cleq 2374  df-clel 2377  df-in 3396  df-ss 3403
This theorem is referenced by:  unissint  4224  resdif  5744  fimacnv  5921  tfrlem5  6967  domss2  7595  dffi3  7806  cantnfp1lem3  8012  cantnfp1lem3OLD  8038  trcl  8072  tcid  8083  r1ordg  8109  r1sssuc  8114  ackbij1lem15  8527  cfsmolem  8563  isfin4-3  8608  fin1a2lem7  8699  wunex2  9027  wuncid  9032  trclfvlb  12846  rtrclreclem1  12893  fsumsplit  13564  o1fsum  13629  fprodsplit  13772  phimullem  14311  vdwlem6  14506  ressinbas  14697  mrcssid  15024  mreexexlem2d  15052  acsfiindd  15924  dirge  15984  symgbasfi  16528  efgredlemf  16876  efgredlemd  16879  gsumzres  17031  gsumzcl2  17032  gsumzf1o  17034  gsumzresOLD  17035  gsumzclOLD  17036  gsumzf1oOLD  17037  gsumzaddlemOLD  17053  gsumadd  17055  gsumaddOLD  17056  gsumzsplit  17061  gsumzsplitOLD  17062  gsumsplit2  17065  gsumzoppgOLD  17084  dprd2da  17204  dmdprdsplit2lem  17207  dmdprdsplit2  17208  dmdprdsplit  17209  dprdsplit  17210  invrpropd  17460  issubdrg  17567  lspssid  17744  aspssid  18095  pjcss  18838  istopon  19511  sscls  19642  ordtbas  19779  cncls2  19860  tgcmp  19987  cmpfi  19994  1stcfb  20031  1stckgenlem  20139  ptbasfi  20167  ptcnplem  20207  ptuncnv  20393  ptunhmeo  20394  fbasrn  20470  cnflf2  20589  fclscmp  20616  alexsublem  20629  ghmcnp  20698  tsmsgsum  20722  tsmsgsumOLD  20725  tsmsresOLD  20730  tsmsres  20731  tsmssplit  20739  tsmsxplem1  20740  ustssco  20802  mopnfss  21031  cnmpt2pc  21513  uniiccdif  22072  uniioombllem3  22079  uniioombllem4  22080  itg2splitlem  22240  itg2split  22241  itgsplit  22327  ellimc2  22366  ellimc3  22368  lhop  22502  plyaddlem1  22695  plymullem1  22696  taylthlem2  22854  mtest  22884  xrlimcnp  23415  fsumharmonic  23458  chtdif  23549  dchrghm  23648  lgsquadlem2  23747  dchrisumlema  23790  dchrisumlem2  23792  dchrisum0lem1b  23817  dchrisum0lem1  23818  pntrlog2bndlem6  23885  pntlemf  23907  ex-res  25283  spanss2  26380  mdsymi  27446  padct  27695  ordtconlem1  28060  issgon  28272  sssigagen  28294  measiuns  28344  sitgclg  28467  cvmliftlem10  28928  ftc1anclem6  30261  heibor1lem  30471  heibor  30483  divrngcl  30526  isdrngo2  30527  igenss  30625  nacsfix  30810  isnumbasgrplem2  31221  rgspnssid  31287  itgpowd  31350  icccncfext  31856  iblsplit  31931  dirkeritg  32050  dirkercncflem2  32052  fourierdlem81  32136  fourierdlem89  32144  fourierdlem91  32146  fourierdlem92  32147  fourierdlem111  32166  fouriercn  32181  srhmsubc  33084  srhmsubcALTV  33103  gsumsplit2f  33154  fdivmpt  33361  fdivpm  33364  refdivpm  33365  paddunssN  35945  sspadd1  35952  sspadd2  35953  pclssidN  36032  diassdvaN  37200  dochvalr  37497  lcdvbase  37733  relexp0a  38241  wnefimgd  38503
  Copyright terms: Public domain W3C validator