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

Theorem syl5sseqr 3333
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 3321 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3256
This theorem is referenced by:  unissint  4009  resdif  5629  fimacnv  5794  domss2  7195  dffi3  7364  cantnfp1lem3  7562  trcl  7590  tcid  7604  r1ordg  7630  r1sssuc  7635  ackbij1lem15  8040  cfsmolem  8076  isfin4-3  8121  fin1a2lem7  8212  wunex2  8539  wuncid  8544  fsumsplit  12453  o1fsum  12512  phimullem  13088  vdwlem6  13274  ressinbas  13445  mrcssid  13762  mreexexlem2d  13790  acsfiindd  14523  dirge  14602  efgredlemf  15293  efgredlemd  15296  gsumzres  15437  gsumzcl  15438  gsumzf1o  15439  gsumzaddlem  15446  gsumadd  15448  gsumzsplit  15449  gsumsplit2  15451  gsumconst  15452  gsumzoppg  15459  dprd2da  15520  dmdprdsplit2lem  15523  dmdprdsplit2  15524  dmdprdsplit  15525  dprdsplit  15526  invrpropd  15723  issubdrg  15813  lspssid  15981  aspssid  16312  pjcss  16859  istopon  16906  sscls  17036  ordtbas  17171  cncls2  17252  tgcmp  17379  cmpfi  17386  1stcfb  17422  1stckgenlem  17499  ptbasfi  17527  ptcnplem  17567  ptuncnv  17753  ptunhmeo  17754  fbasrn  17830  cnflf2  17949  fclscmp  17976  alexsublem  17989  ghmcnp  18058  tsmsgsum  18082  tsmsres  18087  tsmssplit  18095  tsmsxplem1  18096  ustssco  18158  mopnfss  18356  cnmpt2pc  18817  uniiccdif  19330  uniioombllem3  19337  uniioombllem4  19338  itg2splitlem  19500  itg2split  19501  itgsplit  19587  ellimc2  19624  ellimc3  19626  lhop  19760  plyaddlem1  19992  plymullem1  19993  taylthlem2  20150  mtest  20180  xrlimcnp  20667  fsumharmonic  20710  chtdif  20801  dchrghm  20900  lgsquadlem2  20999  dchrisumlema  21042  dchrisumlem2  21044  dchrisum0lem1b  21069  dchrisum0lem1  21070  pntrlog2bndlem6  21137  pntlemf  21159  ex-res  21590  spanss2  22688  mdsymi  23755  issgon  24295  sssigagen  24317  measiuns  24358  cvmliftlem10  24753  rtrclreclem.refl  24916  fprodsplit  25061  heibor1lem  26202  heibor  26214  divrngcl  26257  isdrngo2  26258  igenss  26356  nacsfix  26450  isnumbasgrplem2  26931  rgspnssid  27037  paddunssN  29973  sspadd1  29980  sspadd2  29981  pclssidN  30060  diassdvaN  31226  dochvalr  31523  lcdvbase  31759
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 1661  ax-8 1682  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2361
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 2367  df-cleq 2373  df-clel 2376  df-in 3263  df-ss 3270
  Copyright terms: Public domain W3C validator