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

Theorem syl6sseqr 3397
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 2442 . 2  |-  B  =  C
41, 3syl6sseq 3396 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    C_ wss 3322
This theorem is referenced by:  disjxiun  4211  iunpw  4761  knatar  6082  tfrlem9  6648  tfrlem9a  6649  tfrlem13  6653  tz7.44-2  6667  tz7.44-3  6668  tz7.49  6704  marypha1lem  7440  ordtypelem2  7490  ixpiunwdom  7561  oemapvali  7642  tcss  7685  tcel  7686  pwwf  7735  rankpwi  7751  rankval3b  7754  cplem1  7815  dfac12lem2  8026  infmap2  8100  ackbij1b  8121  ttukeylem6  8396  fpwwe2lem11  8517  fpwwe2lem12  8518  fpwwe2lem13  8519  fpwwe2  8520  uznnssnn  10526  shftfval  11887  rexuzre  12158  climsup  12465  eulerthlem2  13173  ramtlecl  13370  mreexexlem4d  13874  mreexdomd  13876  gsum2d  15548  pgpfac1lem1  15634  pgpfac1lem3a  15636  pgpfac1lem3  15637  pgpfac1lem5  15639  lspsolvlem  16216  lbsextlem2  16233  eltopss  16982  difopn  17100  tgrest  17225  perfopn  17251  pnfnei  17286  mnfnei  17287  regsep2  17442  cncmp  17457  uncmp  17468  hauscmplem  17471  hauscmp  17472  bwth  17475  conndisj  17481  cnconn  17487  concompss  17498  2ndcctbss  17520  islly2  17549  1stckgenlem  17587  txuni2  17599  ptbasfi  17615  ptpjopn  17646  txindis  17668  txtube  17674  hausdiag  17679  xkoinjcn  17721  tgqtop  17746  filcon  17917  elfm2  17982  flimclslem  18018  flffbas  18029  fclsbas  18055  flimfnfcls  18062  alexsubALT  18084  symgtgp  18133  ustssco  18246  isucn2  18311  ucnima  18313  ucnprima  18314  blcls  18538  prdsxmslem2  18561  isngp2  18646  tgioo  18829  xrtgioo  18839  xrsmopn  18845  opnreen  18864  cnheiborlem  18981  cnllycmp  18983  tchcph  19196  uniioombllem4  19480  dyadmbllem  19493  opnmbllem  19495  mbfimaopnlem  19549  mbflimsup  19560  i1fadd  19589  i1fmul  19590  itg1addlem4  19593  i1fmulc  19597  limciun  19783  dvlip2  19881  c1lip3  19885  lhop  19902  dvfsumlem2  19913  dvfsumrlimge0  19916  dvfsumrlim2  19918  ulmval  20298  psercnlem2  20342  efopnlem2  20550  efopn  20551  ubthlem1  22374  issh2  22713  mdsymlem1  23908  xrofsup  24128  gsumpropd2lem  24222  tpr2rico  24312  cvmopnlem  24967  cvmfolem  24968  cvmliftlem6  24979  cvmliftlem8  24981  cvmliftlem13  24985  cvmliftlem15  24987  cvmlift2lem9  25000  cvmlift2lem11  25002  cvmlift2lem12  25003  clim2prod  25218  fprodntriv  25270  trpredpred  25508  trpredtr  25510  trpredrec  25518  wfrlem9  25548  wfrlem12  25551  wfrlem16  25555  frrlem5e  25592  frrlem11  25596  opnmbllem0  26244  cnambfre  26257  comppfsc  26389  filnetlem4  26412  heibor1lem  26520  dsmmacl  27186  dvsconst  27526  dvsid  27527  dvsef  27528  climinf  27710  climsuse  27712  stoweidlem28  27755  stoweidlem50  27777  stoweidlem52  27779  stoweidlem53  27780  stoweidlem54  27781  nbgrassvwo2  28318  iunconlem2  29109  bnj906  29363  bnj1014  29393  bnj1286  29450  bnj1408  29467  bnj1450  29481  bnj1452  29483  bnj1498  29492  bnj1501  29498  osumcllem1N  30815  osumcllem2N  30816  pexmidlem6N  30834  dochexmidlem6  32325  dochexmidlem7  32326  mapdrvallem3  32506
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator