MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sseqtrrdi Structured version   Visualization version   GIF version

Theorem sseqtrrdi 4000
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
sseqtrrdi.1 (𝜑𝐴𝐵)
sseqtrrdi.2 𝐶 = 𝐵
Assertion
Ref Expression
sseqtrrdi (𝜑𝐴𝐶)

Proof of Theorem sseqtrrdi
StepHypRef Expression
1 sseqtrrdi.1 . 2 (𝜑𝐴𝐵)
2 sseqtrrdi.2 . . 3 𝐶 = 𝐵
32eqcomi 2746 . 2 𝐵 = 𝐶
41, 3sseqtrdi 3999 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  abssdv  4030  disjxiun  5107  knatar  7307  iunpw  7710  fviunfun  7882  frrlem8  8229  frrlem10  8231  frrlem12  8233  frrlem14  8235  fprresex  8246  wfrdmclOLD  8268  wfrlem12OLD  8271  wfrlem16OLD  8275  wfrlem17OLD  8276  tfrlem9  8336  tfrlem9a  8337  tfrlem13  8341  tz7.44-2  8358  tz7.44-3  8359  tz7.49  8396  naddcllem  8627  naddov2  8630  naddasslem1  8645  naddasslem2  8646  marypha1lem  9376  ordtypelem2  9462  ixpiunwdom  9533  oemapvali  9627  tcss  9687  tcel  9688  pwwf  9750  rankpwi  9766  rankval3b  9769  cplem1  9832  dfac12lem2  10087  infmap2  10161  ackbij1b  10182  ttukeylem6  10457  fpwwe2lem10  10583  fpwwe2lem11  10584  fpwwe2lem12  10585  fpwwe2  10586  uznnssnn  12827  pfxccatpfx2  14632  shftfval  14962  rexuzre  15244  climsup  15561  clim2prod  15780  fprodntriv  15832  eulerthlem2  16661  ramtlecl  16879  mreexexlem4d  17534  mreexdomd  17536  gsumpropd2lem  18541  gsumzaddlem  19705  gsum2d  19756  telgsums  19777  pgpfac1lem1  19860  pgpfac1lem3a  19862  pgpfac1lem3  19863  pgpfac1lem5  19865  lspsolvlem  20619  lbsextlem2  20636  dsmmacl  21163  eltopss  22272  difopn  22401  tgrest  22526  perfopn  22552  pnfnei  22587  mnfnei  22588  regsep2  22743  cncmp  22759  uncmp  22770  hauscmplem  22773  hauscmp  22774  conndisj  22783  cnconn  22789  conncompss  22800  2ndcctbss  22822  islly2  22851  comppfsc  22899  1stckgenlem  22920  txuni2  22932  ptbasfi  22948  ptpjopn  22979  txindis  23001  txtube  23007  hausdiag  23012  xkoinjcn  23054  tgqtop  23079  filconn  23250  elfm2  23315  flimclslem  23351  flffbas  23362  fclsbas  23388  flimfnfcls  23395  alexsubALT  23418  symgtgp  23473  ustssco  23582  isucn2  23647  ucnima  23649  ucnprima  23650  blcls  23878  prdsxmslem2  23901  isngp2  23969  tgioo  24175  xrtgioo  24185  xrsmopn  24191  opnreen  24210  cnheiborlem  24333  cnllycmp  24335  tcphcph  24617  rrxmvallem  24784  uniioombllem4  24966  dyadmbllem  24979  opnmbllem  24981  mbfimaopnlem  25035  mbflimsup  25046  i1fadd  25075  i1fmul  25076  itg1addlem4  25079  itg1addlem4OLD  25080  i1fmulc  25084  limciun  25274  dvlip2  25375  c1lip3  25379  lhop  25396  dvfsumlem2  25407  dvfsumrlimge0  25410  dvfsumrlim2  25412  ulmval  25755  psercnlem2  25799  efopnlem2  26028  efopn  26029  madebdayim  27239  umgrres1lem  28300  upgrres1  28303  nbgrssvwo2  28352  ubthlem1  29854  issh2  30193  mdsymlem1  31387  padct  31678  xrofsup  31714  fz2ssnn0  31730  zarclsint  32493  tpr2rico  32533  sibfinima  32979  fct2relem  33250  bnj906  33582  bnj1014  33613  bnj1286  33671  bnj1408  33688  bnj1450  33702  bnj1452  33704  bnj1498  33713  bnj1501  33719  lfuhgr  33751  cvmopnlem  33912  cvmfolem  33913  cvmliftlem6  33924  cvmliftlem8  33926  cvmliftlem13  33930  cvmliftlem15  33932  cvmlift2lem9  33945  cvmlift2lem11  33947  cvmlift2lem12  33948  mclsppslem  34217  filnetlem4  34882  dissneqlem  35840  pibt2  35917  lindsdom  36101  opnmbllem0  36143  cnambfre  36155  heibor1lem  36297  osumcllem1N  38448  osumcllem2N  38449  pexmidlem6N  38467  dochexmidlem6  39957  dochexmidlem7  39958  mapdrvallem3  40138  naddwordnexlem4  41747  k0004ss2  42498  cpcolld  42612  dvsconst  42684  dvsid  42685  dvsef  42686  iunconnlem2  43291  uzssd2  43726  climinf  43921  climsuse  43923  climresmpt  43974  climleltrp  43991  stoweidlem28  44343  stoweidlem50  44365  stoweidlem52  44367  stoweidlem53  44368  stoweidlem54  44369  fourierdlem54  44475  fourierdlem80  44501  meaiininclem  44801  caratheodorylem2  44842  hspmbllem2  44942  mbfresmf  45054  smfmbfcex  45075  smflimlem2  45087  smflimsuplem2  45136  smflimsuplem3  45137  smflimsuplem5  45139  smflimsuplem6  45140  isomuspgrlem2c  46096  upgredgssspr  46119  setrec1  47210  setrecsres  47221  aacllem  47322
  Copyright terms: Public domain W3C validator