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

Theorem syl6sseqr 3238
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 2300 . 2  |-  B  =  C
41, 3syl6sseq 3237 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165
This theorem is referenced by:  disjxiun  4036  iunpw  4586  knatar  5873  tfrlem9  6417  tfrlem9a  6418  tfrlem13  6422  tz7.44-2  6436  tz7.44-3  6437  tz7.49  6473  marypha1lem  7202  ordtypelem2  7250  ixpiunwdom  7321  oemapvali  7402  tcss  7445  tcel  7446  pwwf  7495  rankpwi  7511  rankval3b  7514  cplem1  7575  dfac12lem2  7786  infmap2  7860  ackbij1b  7881  ttukeylem6  8157  fpwwe2lem11  8278  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  uznnssnn  10282  shftfval  11581  rexuzre  11852  climsup  12159  eulerthlem2  12866  ramtlecl  13063  mreexexlem4d  13565  mreexdomd  13567  gsum2d  15239  pgpfac1lem1  15325  pgpfac1lem3a  15327  pgpfac1lem3  15328  pgpfac1lem5  15330  lspsolvlem  15911  lbsextlem2  15928  eltopss  16669  difopn  16787  tgrest  16906  perfopn  16931  pnfnei  16966  mnfnei  16967  regsep2  17120  cncmp  17135  uncmp  17146  hauscmplem  17149  hauscmp  17150  conndisj  17158  cnconn  17164  concompss  17175  2ndcctbss  17197  islly2  17226  1stckgenlem  17264  txuni2  17276  ptbasfi  17292  ptpjopn  17322  txindis  17344  txtube  17350  hausdiag  17355  xkoinjcn  17397  tgqtop  17419  filcon  17594  elfm2  17659  flimclslem  17695  flffbas  17706  fclsbas  17732  flimfnfcls  17739  alexsubALT  17761  symgtgp  17800  blcls  18068  prdsxmslem2  18091  isngp2  18135  tgioo  18318  xrtgioo  18328  xrsmopn  18334  opnreen  18352  cnheiborlem  18468  cnllycmp  18470  tchcph  18683  uniioombllem4  18957  dyadmbllem  18970  opnmbllem  18972  mbfimaopnlem  19026  mbflimsup  19037  i1fadd  19066  i1fmul  19067  itg1addlem4  19070  i1fmulc  19074  limciun  19260  dvlip2  19358  c1lip3  19362  lhop  19379  dvfsumlem2  19390  dvfsumrlimge0  19393  dvfsumrlim2  19395  ulmval  19775  psercnlem2  19816  efopnlem2  20020  efopn  20021  ubthlem1  21465  issh2  21804  mdsymlem1  22999  xrofsup  23270  tpr2rico  23311  lmxrge0  23390  gsumpropd2lem  23394  cvmopnlem  23824  cvmfolem  23825  cvmliftlem6  23836  cvmliftlem8  23838  cvmliftlem13  23842  cvmliftlem15  23844  cvmlift2lem9  23857  cvmlift2lem11  23859  cvmlift2lem12  23860  trpredpred  24302  trpredtr  24304  trpredrec  24312  wfrlem9  24335  wfrlem12  24338  wfrlem16  24342  frrlem5e  24360  frrlem11  24364  imgfldref2  25167  toplat  25393  osneisi  25634  elsubops  25635  bwt2  25695  comppfsc  26410  filnetlem4  26433  heibor1lem  26636  dsmmacl  27310  dvsconst  27650  dvsid  27651  dvsef  27652  climinf  27835  climsuse  27837  stoweidlem28  27880  stoweidlem50  27902  stoweidlem52  27904  stoweidlem53  27905  stoweidlem54  27906  bnj906  29278  bnj1014  29308  bnj1286  29365  bnj1408  29382  bnj1450  29396  bnj1452  29398  bnj1498  29407  bnj1501  29413  osumcllem1N  30767  osumcllem2N  30768  pexmidlem6N  30786  dochexmidlem6  32277  dochexmidlem7  32278  mapdrvallem3  32458
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator