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

Theorem syl6sseqr 3225
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 2287 . 2  |-  B  =  C
41, 3syl6sseq 3224 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    C_ wss 3152
This theorem is referenced by:  disjxiun  4020  iunpw  4570  knatar  5857  tfrlem9  6401  tfrlem9a  6402  tfrlem13  6406  tz7.44-2  6420  tz7.44-3  6421  tz7.49  6457  marypha1lem  7186  ordtypelem2  7234  ixpiunwdom  7305  oemapvali  7386  tcss  7429  tcel  7430  pwwf  7479  rankpwi  7495  rankval3b  7498  cplem1  7559  dfac12lem2  7770  infmap2  7844  ackbij1b  7865  ttukeylem6  8141  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  uznnssnn  10266  shftfval  11565  rexuzre  11836  climsup  12143  eulerthlem2  12850  ramtlecl  13047  mreexexlem4d  13549  mreexdomd  13551  gsum2d  15223  pgpfac1lem1  15309  pgpfac1lem3a  15311  pgpfac1lem3  15312  pgpfac1lem5  15314  lspsolvlem  15895  lbsextlem2  15912  eltopss  16653  difopn  16771  tgrest  16890  perfopn  16915  pnfnei  16950  mnfnei  16951  regsep2  17104  cncmp  17119  uncmp  17130  hauscmplem  17133  hauscmp  17134  conndisj  17142  cnconn  17148  concompss  17159  2ndcctbss  17181  islly2  17210  1stckgenlem  17248  txuni2  17260  ptbasfi  17276  ptpjopn  17306  txindis  17328  txtube  17334  hausdiag  17339  xkoinjcn  17381  tgqtop  17403  filcon  17578  elfm2  17643  flimclslem  17679  flffbas  17690  fclsbas  17716  flimfnfcls  17723  alexsubALT  17745  symgtgp  17784  blcls  18052  prdsxmslem2  18075  isngp2  18119  tgioo  18302  xrtgioo  18312  xrsmopn  18318  opnreen  18336  cnheiborlem  18452  cnllycmp  18454  tchcph  18667  uniioombllem4  18941  dyadmbllem  18954  opnmbllem  18956  mbfimaopnlem  19010  mbflimsup  19021  i1fadd  19050  i1fmul  19051  itg1addlem4  19054  i1fmulc  19058  limciun  19244  dvlip2  19342  c1lip3  19346  lhop  19363  dvfsumlem2  19374  dvfsumrlimge0  19377  dvfsumrlim2  19379  ulmval  19759  psercnlem2  19800  efopnlem2  20004  efopn  20005  ubthlem1  21449  issh2  21788  mdsymlem1  22983  xrofsup  23255  tpr2rico  23296  lmxrge0  23375  gsumpropd2lem  23379  cvmopnlem  23809  cvmfolem  23810  cvmliftlem6  23821  cvmliftlem8  23823  cvmliftlem13  23827  cvmliftlem15  23829  cvmlift2lem9  23842  cvmlift2lem11  23844  cvmlift2lem12  23845  trpredpred  24231  trpredtr  24233  trpredrec  24241  wfrlem9  24264  wfrlem12  24267  wfrlem16  24271  frrlem5e  24289  frrlem11  24293  imgfldref2  25064  toplat  25290  osneisi  25531  elsubops  25532  bwt2  25592  comppfsc  26307  filnetlem4  26330  heibor1lem  26533  dsmmacl  27207  dvsconst  27547  dvsid  27548  dvsef  27549  climinf  27732  climsuse  27734  stoweidlem28  27777  stoweidlem50  27799  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  bnj906  28962  bnj1014  28992  bnj1286  29049  bnj1408  29066  bnj1450  29080  bnj1452  29082  bnj1498  29091  bnj1501  29097  osumcllem1N  30145  osumcllem2N  30146  pexmidlem6N  30164  dochexmidlem6  31655  dochexmidlem7  31656  mapdrvallem3  31836
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-in 3159  df-ss 3166
  Copyright terms: Public domain W3C validator