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

Theorem syl5sseqr 3538
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 3526 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-in 3468  df-ss 3475
This theorem is referenced by:  unissint  4296  resdif  5826  fimacnv  6004  tfrlem5  7051  domss2  7678  dffi3  7893  cantnfp1lem3  8102  cantnfp1lem3OLD  8128  trcl  8162  tcid  8173  r1ordg  8199  r1sssuc  8204  ackbij1lem15  8617  cfsmolem  8653  isfin4-3  8698  fin1a2lem7  8789  wunex2  9119  wuncid  9124  fsumsplit  13544  o1fsum  13609  fprodsplit  13752  phimullem  14291  vdwlem6  14486  ressinbas  14675  mrcssid  14996  mreexexlem2d  15024  acsfiindd  15786  dirge  15846  symgbasfi  16390  efgredlemf  16738  efgredlemd  16741  gsumzres  16893  gsumzcl2  16894  gsumzf1o  16896  gsumzresOLD  16897  gsumzclOLD  16898  gsumzf1oOLD  16899  gsumzaddlemOLD  16915  gsumadd  16917  gsumaddOLD  16918  gsumzsplit  16923  gsumzsplitOLD  16924  gsumsplit2  16927  gsumsplit2OLD  16928  gsumzoppgOLD  16947  dprd2da  17070  dmdprdsplit2lem  17073  dmdprdsplit2  17074  dmdprdsplit  17075  dprdsplit  17076  invrpropd  17326  issubdrg  17433  lspssid  17610  aspssid  17961  pjcss  18725  istopon  19404  sscls  19535  ordtbas  19671  cncls2  19752  tgcmp  19879  cmpfi  19886  1stcfb  19924  1stckgenlem  20032  ptbasfi  20060  ptcnplem  20100  ptuncnv  20286  ptunhmeo  20287  fbasrn  20363  cnflf2  20482  fclscmp  20509  alexsublem  20522  ghmcnp  20591  tsmsgsum  20615  tsmsgsumOLD  20618  tsmsresOLD  20623  tsmsres  20624  tsmssplit  20632  tsmsxplem1  20633  ustssco  20695  mopnfss  20924  cnmpt2pc  21406  uniiccdif  21965  uniioombllem3  21972  uniioombllem4  21973  itg2splitlem  22133  itg2split  22134  itgsplit  22220  ellimc2  22259  ellimc3  22261  lhop  22395  plyaddlem1  22588  plymullem1  22589  taylthlem2  22747  mtest  22777  xrlimcnp  23276  fsumharmonic  23319  chtdif  23410  dchrghm  23509  lgsquadlem2  23608  dchrisumlema  23651  dchrisumlem2  23653  dchrisum0lem1b  23678  dchrisum0lem1  23679  pntrlog2bndlem6  23746  pntlemf  23768  ex-res  25140  spanss2  26241  mdsymi  27308  ordtconlem1  27884  issgon  28101  sssigagen  28123  measiuns  28166  sitgclg  28262  cvmliftlem10  28717  rtrclreclem.refl  29045  ftc1anclem6  30071  heibor1lem  30281  heibor  30293  divrngcl  30336  isdrngo2  30337  igenss  30435  nacsfix  30620  isnumbasgrplem2  31029  rgspnssid  31095  itgpowd  31158  icccncfext  31644  iblsplit  31719  dirkeritg  31838  dirkercncflem2  31840  fourierdlem81  31924  fourierdlem89  31932  fourierdlem91  31934  fourierdlem92  31935  fourierdlem111  31954  fouriercn  31969  srhmsubc  32752  srhmsubcOLD  32771  gsumsplit2f  32822  paddunssN  35407  sspadd1  35414  sspadd2  35415  pclssidN  35494  diassdvaN  36662  dochvalr  36959  lcdvbase  37195  wnefimgd  37778
  Copyright terms: Public domain W3C validator