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

Theorem syl6sseqr 3355
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 2408 . 2  |-  B  =  C
41, 3syl6sseq 3354 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649    C_ wss 3280
This theorem is referenced by:  disjxiun  4169  iunpw  4718  knatar  6039  tfrlem9  6605  tfrlem9a  6606  tfrlem13  6610  tz7.44-2  6624  tz7.44-3  6625  tz7.49  6661  marypha1lem  7396  ordtypelem2  7444  ixpiunwdom  7515  oemapvali  7596  tcss  7639  tcel  7640  pwwf  7689  rankpwi  7705  rankval3b  7708  cplem1  7769  dfac12lem2  7980  infmap2  8054  ackbij1b  8075  ttukeylem6  8350  fpwwe2lem11  8471  fpwwe2lem12  8472  fpwwe2lem13  8473  fpwwe2  8474  uznnssnn  10480  shftfval  11840  rexuzre  12111  climsup  12418  eulerthlem2  13126  ramtlecl  13323  mreexexlem4d  13827  mreexdomd  13829  gsum2d  15501  pgpfac1lem1  15587  pgpfac1lem3a  15589  pgpfac1lem3  15590  pgpfac1lem5  15592  lspsolvlem  16169  lbsextlem2  16186  eltopss  16935  difopn  17053  tgrest  17177  perfopn  17203  pnfnei  17238  mnfnei  17239  regsep2  17394  cncmp  17409  uncmp  17420  hauscmplem  17423  hauscmp  17424  conndisj  17432  cnconn  17438  concompss  17449  2ndcctbss  17471  islly2  17500  1stckgenlem  17538  txuni2  17550  ptbasfi  17566  ptpjopn  17597  txindis  17619  txtube  17625  hausdiag  17630  xkoinjcn  17672  tgqtop  17697  filcon  17868  elfm2  17933  flimclslem  17969  flffbas  17980  fclsbas  18006  flimfnfcls  18013  alexsubALT  18035  symgtgp  18084  ustssco  18197  isucn2  18262  ucnima  18264  ucnprima  18265  blcls  18489  prdsxmslem2  18512  isngp2  18597  tgioo  18780  xrtgioo  18790  xrsmopn  18796  opnreen  18815  cnheiborlem  18932  cnllycmp  18934  tchcph  19147  uniioombllem4  19431  dyadmbllem  19444  opnmbllem  19446  mbfimaopnlem  19500  mbflimsup  19511  i1fadd  19540  i1fmul  19541  itg1addlem4  19544  i1fmulc  19548  limciun  19734  dvlip2  19832  c1lip3  19836  lhop  19853  dvfsumlem2  19864  dvfsumrlimge0  19867  dvfsumrlim2  19869  ulmval  20249  psercnlem2  20293  efopnlem2  20501  efopn  20502  ubthlem1  22325  issh2  22664  mdsymlem1  23859  xrofsup  24079  gsumpropd2lem  24173  tpr2rico  24263  cvmopnlem  24918  cvmfolem  24919  cvmliftlem6  24930  cvmliftlem8  24932  cvmliftlem13  24936  cvmliftlem15  24938  cvmlift2lem9  24951  cvmlift2lem11  24953  cvmlift2lem12  24954  clim2prod  25169  fprodntriv  25221  trpredpred  25445  trpredtr  25447  trpredrec  25455  wfrlem9  25478  wfrlem12  25481  wfrlem16  25485  frrlem5e  25503  frrlem11  25507  mblfinlem  26143  cnambfre  26154  comppfsc  26277  filnetlem4  26300  heibor1lem  26408  dsmmacl  27075  dvsconst  27415  dvsid  27416  dvsef  27417  climinf  27599  climsuse  27601  stoweidlem28  27644  stoweidlem50  27666  stoweidlem52  27668  stoweidlem53  27669  stoweidlem54  27670  bnj906  29007  bnj1014  29037  bnj1286  29094  bnj1408  29111  bnj1450  29125  bnj1452  29127  bnj1498  29136  bnj1501  29142  osumcllem1N  30438  osumcllem2N  30439  pexmidlem6N  30457  dochexmidlem6  31948  dochexmidlem7  31949  mapdrvallem3  32129
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 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
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 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator