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

Theorem syl6sseqr 3395
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
syl6ssr.1  |-  ( ph  ->  A  C_  B )
syl6ssr.2  |-  C  =  B
Assertion
Ref Expression
syl6sseqr  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl6sseqr
StepHypRef Expression
1 syl6ssr.1 . 2  |-  ( ph  ->  A  C_  B )
2 syl6ssr.2 . . 3  |-  C  =  B
32eqcomi 2440 . 2  |-  B  =  C
41, 3syl6sseq 3394 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    C_ wss 3320
This theorem is referenced by:  disjxiun  4209  iunpw  4759  knatar  6080  tfrlem9  6646  tfrlem9a  6647  tfrlem13  6651  tz7.44-2  6665  tz7.44-3  6666  tz7.49  6702  marypha1lem  7438  ordtypelem2  7488  ixpiunwdom  7559  oemapvali  7640  tcss  7683  tcel  7684  pwwf  7733  rankpwi  7749  rankval3b  7752  cplem1  7813  dfac12lem2  8024  infmap2  8098  ackbij1b  8119  ttukeylem6  8394  fpwwe2lem11  8515  fpwwe2lem12  8516  fpwwe2lem13  8517  fpwwe2  8518  uznnssnn  10524  shftfval  11885  rexuzre  12156  climsup  12463  eulerthlem2  13171  ramtlecl  13368  mreexexlem4d  13872  mreexdomd  13874  gsum2d  15546  pgpfac1lem1  15632  pgpfac1lem3a  15634  pgpfac1lem3  15635  pgpfac1lem5  15637  lspsolvlem  16214  lbsextlem2  16231  eltopss  16980  difopn  17098  tgrest  17223  perfopn  17249  pnfnei  17284  mnfnei  17285  regsep2  17440  cncmp  17455  uncmp  17466  hauscmplem  17469  hauscmp  17470  bwth  17473  conndisj  17479  cnconn  17485  concompss  17496  2ndcctbss  17518  islly2  17547  1stckgenlem  17585  txuni2  17597  ptbasfi  17613  ptpjopn  17644  txindis  17666  txtube  17672  hausdiag  17677  xkoinjcn  17719  tgqtop  17744  filcon  17915  elfm2  17980  flimclslem  18016  flffbas  18027  fclsbas  18053  flimfnfcls  18060  alexsubALT  18082  symgtgp  18131  ustssco  18244  isucn2  18309  ucnima  18311  ucnprima  18312  blcls  18536  prdsxmslem2  18559  isngp2  18644  tgioo  18827  xrtgioo  18837  xrsmopn  18843  opnreen  18862  cnheiborlem  18979  cnllycmp  18981  tchcph  19194  uniioombllem4  19478  dyadmbllem  19491  opnmbllem  19493  mbfimaopnlem  19547  mbflimsup  19558  i1fadd  19587  i1fmul  19588  itg1addlem4  19591  i1fmulc  19595  limciun  19781  dvlip2  19879  c1lip3  19883  lhop  19900  dvfsumlem2  19911  dvfsumrlimge0  19914  dvfsumrlim2  19916  ulmval  20296  psercnlem2  20340  efopnlem2  20548  efopn  20549  ubthlem1  22372  issh2  22711  mdsymlem1  23906  xrofsup  24126  gsumpropd2lem  24220  tpr2rico  24310  cvmopnlem  24965  cvmfolem  24966  cvmliftlem6  24977  cvmliftlem8  24979  cvmliftlem13  24983  cvmliftlem15  24985  cvmlift2lem9  24998  cvmlift2lem11  25000  cvmlift2lem12  25001  clim2prod  25216  fprodntriv  25268  trpredpred  25506  trpredtr  25508  trpredrec  25516  wfrlem9  25546  wfrlem12  25549  wfrlem16  25553  frrlem5e  25590  frrlem11  25594  opnmbllem0  26242  cnambfre  26255  comppfsc  26387  filnetlem4  26410  heibor1lem  26518  dsmmacl  27184  dvsconst  27524  dvsid  27525  dvsef  27526  climinf  27708  climsuse  27710  stoweidlem28  27753  stoweidlem50  27775  stoweidlem52  27777  stoweidlem53  27778  stoweidlem54  27779  iunconlem2  29047  bnj906  29301  bnj1014  29331  bnj1286  29388  bnj1408  29405  bnj1450  29419  bnj1452  29421  bnj1498  29430  bnj1501  29436  osumcllem1N  30753  osumcllem2N  30754  pexmidlem6N  30772  dochexmidlem6  32263  dochexmidlem7  32264  mapdrvallem3  32444
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator