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

Theorem syl5sseqr 3426
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 3414 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369    C_ wss 3349
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3356  df-ss 3363
This theorem is referenced by:  unissint  4173  resdif  5682  fimacnv  5856  tfrlem5  6860  domss2  7491  dffi3  7702  cantnfp1lem3  7909  cantnfp1lem3OLD  7935  trcl  7969  tcid  7980  r1ordg  8006  r1sssuc  8011  ackbij1lem15  8424  cfsmolem  8460  isfin4-3  8505  fin1a2lem7  8596  wunex2  8926  wuncid  8931  fsumsplit  13237  o1fsum  13297  phimullem  13875  vdwlem6  14068  ressinbas  14255  mrcssid  14576  mreexexlem2d  14604  acsfiindd  15368  dirge  15428  symgbasfi  15912  efgredlemf  16259  efgredlemd  16262  gsumzres  16409  gsumzcl2  16410  gsumzf1o  16412  gsumzresOLD  16413  gsumzclOLD  16414  gsumzf1oOLD  16415  gsumzaddlemOLD  16431  gsumadd  16433  gsumaddOLD  16434  gsumzsplit  16439  gsumzsplitOLD  16440  gsumsplit2  16443  gsumsplit2OLD  16444  gsumzoppgOLD  16463  dprd2da  16563  dmdprdsplit2lem  16566  dmdprdsplit2  16567  dmdprdsplit  16568  dprdsplit  16569  invrpropd  16812  issubdrg  16912  lspssid  17088  aspssid  17426  pjcss  18163  istopon  18552  sscls  18682  ordtbas  18818  cncls2  18899  tgcmp  19026  cmpfi  19033  1stcfb  19071  1stckgenlem  19148  ptbasfi  19176  ptcnplem  19216  ptuncnv  19402  ptunhmeo  19403  fbasrn  19479  cnflf2  19598  fclscmp  19625  alexsublem  19638  ghmcnp  19707  tsmsgsum  19731  tsmsgsumOLD  19734  tsmsresOLD  19739  tsmsres  19740  tsmssplit  19748  tsmsxplem1  19749  ustssco  19811  mopnfss  20040  cnmpt2pc  20522  uniiccdif  21080  uniioombllem3  21087  uniioombllem4  21088  itg2splitlem  21248  itg2split  21249  itgsplit  21335  ellimc2  21374  ellimc3  21376  lhop  21510  plyaddlem1  21703  plymullem1  21704  taylthlem2  21861  mtest  21891  xrlimcnp  22384  fsumharmonic  22427  chtdif  22518  dchrghm  22617  lgsquadlem2  22716  dchrisumlema  22759  dchrisumlem2  22761  dchrisum0lem1b  22786  dchrisum0lem1  22787  pntrlog2bndlem6  22854  pntlemf  22876  ex-res  23670  spanss2  24770  mdsymi  25837  ordtconlem1  26376  issgon  26588  sssigagen  26610  measiuns  26653  cvmliftlem10  27205  rtrclreclem.refl  27368  fprodsplit  27498  ftc1anclem6  28498  heibor1lem  28734  heibor  28746  divrngcl  28789  isdrngo2  28790  igenss  28888  nacsfix  29074  isnumbasgrplem2  29486  rgspnssid  29553  itgpowd  29616  gsumsplit2f  30793  paddunssN  33548  sspadd1  33555  sspadd2  33556  pclssidN  33635  diassdvaN  34801  dochvalr  35098  lcdvbase  35334
  Copyright terms: Public domain W3C validator