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

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

Proof of Theorem eqsstrid
StepHypRef Expression
1 eqsstrid.2 . 2 (𝜑𝐵𝐶)
2 eqsstrid.1 . . 3 𝐴 = 𝐵
32sseq1i 3954 . 2 (𝐴𝐶𝐵𝐶)
41, 3sylibr 233 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wss 3892
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3439  df-in 3899  df-ss 3909
This theorem is referenced by:  eqsstrrid  3975  inss  4178  tpssi  4775  opabssxpd  5645  xpsspw  5731  fun  6666  fmpt  7016  fliftrel  7211  knatar  7260  fr3nr  7654  sucexeloni  7690  suceloniOLD  7692  fiun  7817  f1iun  7818  1stcof  7893  2ndcof  7894  fsplitfpar  7990  fnwelem  8003  oeeui  8464  aceq3lem  9930  cflecard  10063  cfslb2n  10078  itunitc1  10230  axdc3lem2  10261  fpwwe2lem11  10451  canthwelem  10460  wuncval2  10557  peano5nni  12030  un0addcl  12320  un0mulcl  12321  fsuppmapnn0fiublem  13764  fsuppmapnn0fiub  13765  mertenslem2  15650  4sqlem11  16709  4sqlem19  16717  vdwlem13  16747  imasless  17304  rescfth  17706  oppchofcl  18031  oyoncl  18041  mgmidsssn0  18409  cycsubm  18874  efgsfo  19398  efgcpbllemb  19414  frgpuplem  19431  gsummpt1n0  19619  dprdfid  19673  dprd2d2  19700  ablfacrp  19722  ablfac1b  19726  ablfac1eu  19729  pgpfac1lem5  19735  ablfaclem3  19743  lsptpcl  20298  lsppratlem3  20468  lsppratlem4  20469  lbsextlem2  20478  f1lindf  21086  topsn  22137  ordtbaslem  22396  ordtuni  22398  ordtbas2  22399  cnpco  22475  cnconst2  22491  tgcmp  22609  iunconn  22636  ptuni2  22784  xkococnlem  22867  tgqtop  22920  fbasrn  23092  uzrest  23105  fmco  23169  alexsubALT  23259  cnextf  23274  snclseqg  23324  ustund  23430  imasdsf1olem  23583  xmetresbl  23647  blsscls2  23717  metustss  23764  tngtopn  23871  reconn  24048  metnrmlem3  24081  cphsubrglem  24398  minveclem1  24645  minveclem3b  24649  ovolficcss  24690  ovolicc2lem4  24741  iundisj2  24770  uniioombllem4  24807  vitalilem5  24833  mbfeqalem1  24862  itg1addlem4  24920  itg1addlem4OLD  24921  limciun  25115  dvlip2  25216  dv11cn  25222  aalioulem3  25551  pserdvlem2  25644  pserdv  25645  abelthlem2  25648  efif1o  25759  efrlim  26176  lgamgulmlem1  26235  fsumdvdsmul  26401  perfectlem2  26435  setsvtx  27462  uhgredgn0  27555  upgredgss  27559  umgredgss  27560  usgredgss  27586  umgrres1lem  27734  upgrres1  27737  1hegrvtxdg1r  27932  clwlknf1oclwwlknlem3  28504  minvecolem1  29293  sh0le  29859  mdslmd3i  30751  iundisj2f  30986  suppss2f  31031  2ndresdju  31043  fnpreimac  31065  fdifsuppconst  31080  suppss3  31116  iundisj2fi  31175  lsmsnorb  31633  pstmfval  31901  ordtrest2NEW  31928  ldgenpisyslem1  32186  ldgenpisyslem2  32187  omsmeas  32345  sitgclbn  32365  eulerpartlemt  32393  eulerpartlemmf  32397  eulerpartlemgf  32401  bnj849  32960  bnj1136  33032  bnj1311  33059  bnj1413  33070  bnj1452  33087  blsconn  33261  cvmliftlem2  33303  cvmlift2lem12  33331  mvtss  33570  mthmpps  33599  noextendseq  33925  nosupno  33961  nosupbnd2lem1  33973  noinfno  33976  noetasuplem4  33994  neibastop2lem  34604  filnetlem3  34624  finxpsuclem  35622  poimirlem3  35834  mblfinlem3  35870  areacirclem2  35920  sdclem1  35955  istotbnd3  35983  sstotbnd  35987  iccbnd  36052  icccmpALT  36053  osumcllem1N  38176  osumcllem2N  38177  osumcllem4N  38179  osumcllem9N  38184  pexmidlem6N  38195  dihglblem3N  39515  dvhdimlem  39664  dochexmidlem6  39685  lcfrlem16  39778  lcfr  39805  ssabdv  40398  hbtlem6  41159  iocinico  41248  trclubgNEW  41448  cnvrcl0  41455  relexp0a  41546  brtrclfv2  41557  cotrclrcl  41572  frege77d  41576  unhe1  41615  ntrrn  41954  imo72b2lem0  41998  imo72b2lem2  42000  imo72b2  42005  mnuprdlem4  42115  radcnvrat  42154  iunconnlem2  42777  ssinss2d  42830  limccog  43399  limsupresico  43479  liminfresico  43550  icccncfext  43666  stoweidlem14  43793  fourierdlem20  43906  fourierdlem42  43928  fourierdlem46  43931  fourierdlem50  43935  fourierdlem51  43936  fourierdlem54  43939  fourierdlem64  43949  fourierdlem76  43961  fourierdlem102  43987  fourierdlem103  43988  fourierdlem104  43989  fourierdlem114  43999  meadjiunlem  44242  meaiininclem  44263  ovnsupge0  44334  hoidmvlelem2  44373  hoidmvlelem4  44375  vonvolmbllem  44437  vonvolmbl2  44440  vonvol2  44441  vonioolem1  44457  issmflem  44504  fundcmpsurinjimaid  45116  perfectALTVlem2  45427  uspgropssxp  45559  funcrngcsetc  45809  funcringcsetc  45846  srhmsubc  45887  rhmsubclem3  45899  srhmsubcALTV  45905  rhmsubcALTVlem4  45918  setrec2fun  46651  onsetreclem2  46664
  Copyright terms: Public domain W3C validator