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

Theorem eqsstrdi 3997
Description: A chained subclass and equality deduction. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
eqsstrdi.1 (𝜑𝐴 = 𝐵)
eqsstrdi.2 𝐵𝐶
Assertion
Ref Expression
eqsstrdi (𝜑𝐴𝐶)

Proof of Theorem eqsstrdi
StepHypRef Expression
1 eqsstrdi.1 . 2 (𝜑𝐴 = 𝐵)
2 eqsstrdi.2 . . 3 𝐵𝐶
32a1i 11 . 2 (𝜑𝐵𝐶)
41, 3eqsstrd 3981 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3909
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 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-in 3916  df-ss 3926
This theorem is referenced by:  eqsstrrdi  3998  dmxpss  6120  dmsnopss  6163  iotassuni  6464  iotassuniOLD  6471  fvmptss  6956  fvmptss2  6969  fimacnvOLD  7017  funressn  7100  riotassuni  7347  ordsuci  7734  frxp  8047  suppssdm  8076  suppun  8083  suppss  8093  suppssOLD  8094  suppssov1  8097  suppss2  8099  suppssfv  8101  wfrlem15OLD  8237  oawordeulem  8469  omwordri  8487  oewordri  8507  mapssfset  8723  fodomr  9006  fipwuni  9296  fipwss  9299  ordtypelem6  9393  inf3lemd  9497  cantnfle  9541  cantnflem2  9560  ttrclselem1  9595  en2other2  9879  ackbij1lem15  10104  ackbij2lem3  10111  cfub  10119  cflecard  10123  cfle  10124  fin23lem13  10202  fin23lem29  10211  compsscnvlem  10240  itunitc1  10290  fpwwe2lem11  10511  grur1a  10689  uzssz  12717  fsuppmapnn0fiublem  13824  fsuppmapnn0fiub  13825  swrdlend  14473  repswswrd  14604  cshimadifsn  14650  xptrrel  14799  relexpnndm  14860  relexpdmd  14863  relexprnd  14867  relexpfldd  14869  rtrclreclem4  14880  limsupgle  15294  isercolllem2  15485  isercolllem3  15486  isercoll  15487  fsumss  15545  sadcaddlem  16272  sadadd2lem  16274  sadadd3  16276  sadcl  16277  sadaddlem  16281  sadasslem  16285  sadeq  16287  smupvallem  16298  smucl  16299  prmreclem4  16726  prmreclem5  16727  1arith  16734  vdwmc2  16786  vdwlem13  16800  ramz2  16831  strfvss  16994  ressbasss  17056  prdsless  17280  sectss  17570  invss  17579  fullfunc  17728  fthfunc  17729  catccatid  17927  resscatc  17930  catcisolem  17931  catciso  17932  yoniso  18109  gsumpropd2lem  18469  cntzrcl  19039  cntzssv  19040  gsumzmhm  19643  ablfaclem3  19795  lmhmlsp  20433  evpmss  20913  cssss  21012  frlmplusgval  21093  frlmvscafval  21095  uvcresum  21122  resspsrbas  21306  resspsrvsca  21309  subrgpsr  21310  mplsubglem  21327  ressmplbas  21351  subrgmpl  21355  mpfrcl  21417  ressply1bas  21522  scmatlss  21796  cpmatsubgpmat  21991  toponsspwpw  22193  basdif0  22225  ntrss2  22330  ordtbas2  22464  ordtbas  22465  cncls  22547  cmpfi  22681  comppfsc  22805  kgentopon  22811  ptpjpre1  22844  xkoccn  22892  prdstopn  22901  uzfbas  23171  utoptop  23508  utopbas  23509  setsmstopn  23755  restmetu  23848  tngtopn  23936  iccntr  24106  metdstri  24136  pi1xfrcnvlem  24341  cphsubrglem  24463  tcphcph  24523  rrxnm  24677  rrxbasefi  24696  ovolshftlem1  24795  ovolshft  24797  ovolscalem1  24799  ovolscalem2  24800  ovolsca  24801  uniioombllem2  24869  uniioombllem3a  24870  uniioombllem3  24871  uniioombllem4  24872  uniioombllem6  24874  itgioo  25102  limcnlp  25164  dvbsss  25188  dvcnvrelem1  25303  dvfsumle  25307  dvfsumabs  25309  pserdv  25710  rlimcnp2  26238  fsumharmonic  26283  chpval2  26488  bday0b  27091  madef  27107  madess  27126  oldssmade  27127  tglnssp  27280  perpln1  27438  perpln2  27439  uhgrspansubgr  28025  clwwlknclwwlkdifnum  28710  ocsh  30011  shsss  30041  speccl  30627  elnlfn  30656  pj3i  30936  sumdmdlem2  31147  fcoinver  31310  ffsrn  31428  ssnnssfz  31472  pfxrn2  31578  cycpmrn  31774  cycpmconjslem2  31786  inftmrel  31798  ressply1evl  32047  evls1muld  32048  ressply1mon1p  32052  minplyeulem  32134  smatrcl  32138  metidss  32233  fsumcvg4  32292  dya2iocuni  32644  carsgcl  32665  breprexplema  33004  bnj1143  33163  bnj1262  33183  bnj517  33258  kur14lem1  33561  cvmliftmolem2  33637  cvmliftlem15  33653  mrsubrn  33868  msubrn  33884  poimirlem30  35994  mblfinlem2  36002  sdclem2  36087  sstotbnd2  36119  isbnd3  36129  lkrlss  37443  pmapssat  38108  diass  39391  diaintclN  39407  dia2dimlem13  39425  dibintclN  39516  lcfrlem25  39916  lcdvbasess  39943  mapdin  40011  eqimssd  40521  ressbasssg  40553  diophin  40929  rmxyelqirr  41067  itgocn  41325  oacl2g  41390  ofoafg  41394  ofoaf  41395  fpwfvss  41415  relexp0a  41719  frege131d  41767  fsovrfovd  42012  clsk1indlem2  42047  clsk1indlem3  42048  mnuprd  42289  unirestss  43067  founiiun0  43135  fsumsupp0  43541  limsupequzlem  43685  ibliooicc  43934  stoweidlem34  43997  stoweidlem59  44022  etransclem24  44221  caratheodory  44491  ovnhoilem1  44564  hspdifhsp  44579  smfaddlem2  44727  smflimlem1  44734  smflimlem2  44735  smfmullem4  44757  smfsuplem1  44774  fcoreslem4  45018  fcoresf1  45021  fcoresfo  45023  rnghmresfn  45979  dfrngc2  45988  rnghmsscmap2  45989  rnghmsscmap  45990  rngchomrnghmresALTV  46012  funcrngcsetc  46014  rhmresfn  46025  dfringc2  46034  rhmsscmap2  46035  rhmsscmap  46036  rhmsscrnghm  46042  funcringcsetc  46051  funcringcsetcALTV2lem9  46060  rngcrescrhm  46101  rhmsubclem1  46102  rhmsubclem4  46105  rngcrescrhmALTV  46119  rhmsubcALTVlem1  46120  ssnn0ssfz  46143  isclatd  46726  setrec2fun  46855
  Copyright terms: Public domain W3C validator