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

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

Proof of Theorem eqsstrrid
StepHypRef Expression
1 eqsstrrid.1 . . 3 𝐵 = 𝐴
21eqcomi 2746 . 2 𝐴 = 𝐵
3 eqsstrrid.2 . 2 (𝜑𝐵𝐶)
42, 3eqsstrid 3949 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1543  wss 3866
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708
This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873  df-ss 3883
This theorem is referenced by:  relcnvtrg  6130  fimacnvdisj  6597  dffv2  6806  fimacnvOLD  6891  f1ompt  6928  abnexg  7541  fnwelem  7898  tfrlem15  8128  omxpenlem  8746  hartogslem1  9158  infxpidm2  9631  alephgeom  9696  infenaleph  9705  cfflb  9873  pwfseqlem5  10277  imasvscafn  17042  mrieqvlemd  17132  cnvps  18084  dirdm  18106  tsrdir  18110  frmdss2  18290  subdrgint  19847  iinopn  21799  neitr  22077  xkococnlem  22556  tgpconncomp  23010  trcfilu  23191  mbfconstlem  24524  itg2seq  24640  limcdif  24773  dvres2lem  24807  c1lip3  24896  lhop  24913  plyeq0  25105  dchrghm  26137  uspgrupgrushgr  27268  upgrreslem  27392  umgrreslem  27393  umgrres1  27402  umgr2v2e  27613  chssoc  29577  gsumhashmul  31035  pmtrcnelor  31079  tocycfvres1  31096  tocycfvres2  31097  dimkerim  31422  hauseqcn  31562  carsgclctunlem3  31999  cvmliftmolem1  32956  cvmlift2lem9a  32978  cvmlift2lem9  32986  ttrcltr  33515  dfttrcl2  33523  cnres2  35658  rngunsnply  40701  proot1hash  40728  clcnvlem  40907  cnvtrcl0  40910  trrelsuperrel2dg  40956  brtrclfv2  41012  imo72b2lem1  41457  fourierdlem92  43414  vsetrec  46079
  Copyright terms: Public domain W3C validator