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

Theorem syl5sseqr 3357
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 3345 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3280
This theorem is referenced by:  unissint  4034  resdif  5655  fimacnv  5821  domss2  7225  dffi3  7394  cantnfp1lem3  7592  trcl  7620  tcid  7634  r1ordg  7660  r1sssuc  7665  ackbij1lem15  8070  cfsmolem  8106  isfin4-3  8151  fin1a2lem7  8242  wunex2  8569  wuncid  8574  fsumsplit  12488  o1fsum  12547  phimullem  13123  vdwlem6  13309  ressinbas  13480  mrcssid  13797  mreexexlem2d  13825  acsfiindd  14558  dirge  14637  efgredlemf  15328  efgredlemd  15331  gsumzres  15472  gsumzcl  15473  gsumzf1o  15474  gsumzaddlem  15481  gsumadd  15483  gsumzsplit  15484  gsumsplit2  15486  gsumconst  15487  gsumzoppg  15494  dprd2da  15555  dmdprdsplit2lem  15558  dmdprdsplit2  15559  dmdprdsplit  15560  dprdsplit  15561  invrpropd  15758  issubdrg  15848  lspssid  16016  aspssid  16347  pjcss  16898  istopon  16945  sscls  17075  ordtbas  17210  cncls2  17291  tgcmp  17418  cmpfi  17425  1stcfb  17461  1stckgenlem  17538  ptbasfi  17566  ptcnplem  17606  ptuncnv  17792  ptunhmeo  17793  fbasrn  17869  cnflf2  17988  fclscmp  18015  alexsublem  18028  ghmcnp  18097  tsmsgsum  18121  tsmsres  18126  tsmssplit  18134  tsmsxplem1  18135  ustssco  18197  mopnfss  18426  cnmpt2pc  18906  uniiccdif  19423  uniioombllem3  19430  uniioombllem4  19431  itg2splitlem  19593  itg2split  19594  itgsplit  19680  ellimc2  19717  ellimc3  19719  lhop  19853  plyaddlem1  20085  plymullem1  20086  taylthlem2  20243  mtest  20273  xrlimcnp  20760  fsumharmonic  20803  chtdif  20894  dchrghm  20993  lgsquadlem2  21092  dchrisumlema  21135  dchrisumlem2  21137  dchrisum0lem1b  21162  dchrisum0lem1  21163  pntrlog2bndlem6  21230  pntlemf  21252  ex-res  21702  spanss2  22800  mdsymi  23867  issgon  24459  sssigagen  24481  measiuns  24524  cvmliftlem10  24934  rtrclreclem.refl  25097  fprodsplit  25242  heibor1lem  26408  heibor  26420  divrngcl  26463  isdrngo2  26464  igenss  26562  nacsfix  26656  isnumbasgrplem2  27137  rgspnssid  27243  paddunssN  30290  sspadd1  30297  sspadd2  30298  pclssidN  30377  diassdvaN  31543  dochvalr  31840  lcdvbase  32076
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator