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

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

Proof of Theorem syl6eqss
StepHypRef Expression
1 syl6eqss.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6eqss.2 . . 3 𝐵𝐶
32a1i 11 . 2 (𝜑𝐵𝐶)
41, 3eqsstrd 3598 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wss 3536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-in 3543  df-ss 3550
This theorem is referenced by:  syl6eqssr  3615  dmxpss  5467  dmsnopss  5508  iotassuni  5767  fvmptss  6183  fvmptss2  6194  fimacnv  6237  funressn  6306  riotassuni  6522  frxp  7148  suppssdm  7169  suppun  7176  suppss  7186  suppssov1  7188  suppss2  7190  suppssfv  7192  wfrlem15  7290  oawordeulem  7495  omwordri  7513  oewordri  7533  fodomr  7970  fipwuni  8189  fipwss  8192  ordtypelem6  8285  inf3lemd  8381  cantnfle  8425  cantnflem2  8444  en2other2  8689  ackbij1lem15  8913  ackbij2lem3  8920  cfub  8928  cflecard  8932  cfle  8933  fin23lem13  9011  fin23lem29  9020  compsscnvlem  9049  itunitc1  9099  fpwwe2lem12  9316  grur1a  9494  uzssz  11536  fsuppmapnn0fiublem  12603  fsuppmapnn0fiub  12604  fsuppmapnn0fiubOLD  12605  swrdlend  13226  repswswrd  13325  cshimadifsn  13369  xptrrel  13510  relexpnndm  13572  limsupgle  13999  isercolllem2  14187  isercoll  14189  fsumss  14246  sadcaddlem  14960  sadadd2lem  14962  sadadd3  14964  sadcl  14965  sadaddlem  14969  sadasslem  14973  sadeq  14975  smupvallem  14986  smucl  14987  prmreclem4  15404  prmreclem5  15405  1arith  15412  vdwmc2  15464  vdwlem13  15478  ramz2  15509  strfvss  15656  ressbasss  15702  prdsless  15889  sectss  16178  invss  16187  fullfunc  16332  fthfunc  16333  catccatid  16518  resscatc  16521  catcisolem  16522  catciso  16523  yoniso  16691  gsumpropd2lem  17039  cntzrcl  17526  cntzssv  17527  gsumzmhm  18103  ablfaclem3  18252  lmhmlsp  18813  resspsrbas  19179  resspsrvsca  19182  subrgpsr  19183  mplsubglem  19198  ressmplbas  19220  subrgmpl  19224  mpfrcl  19282  ressply1bas  19363  evpmss  19693  cssss  19787  frlmplusgval  19865  frlmvscafval  19867  uvcresum  19890  scmatlss  20089  cpmatsubgpmat  20283  basdif0  20507  ntrss2  20610  ordtbas2  20744  ordtbas  20745  cncls  20827  cmpfi  20960  comppfsc  21084  kgentopon  21090  ptpjpre1  21123  xkoccn  21171  prdstopn  21180  uzfbas  21451  utoptop  21787  utopbas  21788  setsmstopn  22031  restmetu  22123  tngtopn  22199  iccntr  22361  metdstri  22390  pi1xfrcnvlem  22592  cphsubrglem  22706  tchcph  22762  rrxnm  22901  ovolshftlem1  22998  ovolshft  23000  ovolscalem1  23002  ovolscalem2  23003  ovolsca  23004  uniioombllem2  23071  uniioombllem3a  23072  uniioombllem3  23073  uniioombllem4  23074  uniioombllem6  23076  itgioo  23302  limcnlp  23362  dvbsss  23386  dvcnvrelem1  23498  dvfsumle  23502  dvfsumabs  23504  pserdv  23901  rlimcnp2  24407  fsumharmonic  24452  chpval2  24657  tglnssp  25162  perpln1  25320  perpln2  25321  nbgrassvt  25725  clwwlksswrd  26068  ocsh  27329  shsss  27359  speccl  27945  elnlfn  27974  pj3i  28254  sumdmdlem2  28465  fcoinver  28601  ffsrn  28695  ssnnssfz  28740  inftmrel  28868  smatrcl  28993  metidss  29065  fsumcvg4  29127  dya2iocuni  29475  carsgcl  29496  bnj1143  29918  bnj1262  29938  bnj517  30012  kur14lem1  30245  cvmliftmolem2  30321  cvmliftlem15  30337  mrsubrn  30467  msubrn  30483  trpredlem1  30774  bj-toponss  32041  poimirlem30  32409  mblfinlem2  32417  sdclem2  32508  sstotbnd2  32543  isbnd3  32553  lkrlss  33200  pmapssat  33863  diass  35149  diaintclN  35165  dia2dimlem13  35183  dibintclN  35274  lcfrlem25  35674  lcdvbasess  35701  mapdin  35769  diophin  36154  itgocn  36553  relexp0a  36827  frege131d  36875  fsovrfovd  37123  clsk1indlem2  37160  clsk1indlem3  37161  unirestss  38139  fsumsupp0  38446  ibliooicc  38664  stoweidlem34  38728  stoweidlem59  38753  etransclem24  38952  caratheodory  39219  ovnhoilem1  39292  hspdifhsp  39307  smfaddlem2  39451  smflimlem1  39458  smflimlem2  39459  smfmullem4  39480  uhgrspansubgr  40514  rnghmresfn  41754  rnghmsscmap2  41764  rnghmsscmap  41765  rngchomrnghmresALTV  41787  funcrngcsetc  41789  rhmresfn  41800  dfringc2  41809  rhmsscmap2  41810  rhmsscmap  41811  rhmsscrnghm  41817  funcringcsetc  41826  funcringcsetcALTV2lem9  41835  rngcrescrhm  41876  rhmsubclem1  41877  rhmsubclem4  41880  rngcrescrhmALTV  41895  rhmsubcALTVlem1  41896  ssnn0ssfz  41919
  Copyright terms: Public domain W3C validator