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

Theorem eqsstrrid 4023
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 4022 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1540  wss 3951
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 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2708
This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2729  df-ss 3968
This theorem is referenced by:  3sstr3g  4036  relcnvtrg  6286  fimacnvdisj  6786  dffv2  7004  f1ompt  7131  abnexg  7776  fnwelem  8156  tfrlem15  8432  omxpenlem  9113  hartogslem1  9582  ttrcltr  9756  dfttrcl2  9764  infxpidm2  10057  alephgeom  10122  infenaleph  10131  cfflb  10299  pwfseqlem5  10703  imasvscafn  17582  mrieqvlemd  17672  cnvps  18623  dirdm  18645  tsrdir  18649  frmdss2  18876  subdrgint  20804  iinopn  22908  neitr  23188  xkococnlem  23667  tgpconncomp  24121  trcfilu  24303  mbfconstlem  25662  itg2seq  25777  limcdif  25911  dvres2lem  25945  c1lip3  26038  lhop  26055  plyeq0  26250  dchrghm  27300  negsbdaylem  28088  precsexlem10  28240  uspgrupgrushgr  29196  upgrreslem  29321  umgrreslem  29322  umgrres1  29331  umgr2v2e  29543  chssoc  31515  gsumhashmul  33064  pmtrcnelor  33111  tocycfvres1  33130  tocycfvres2  33131  elrgspnsubrunlem2  33252  dimkerim  33678  hauseqcn  33897  carsgclctunlem3  34322  cvmliftmolem1  35286  cvmlift2lem9a  35308  cvmlift2lem9  35316  cnres2  37770  rngunsnply  43181  proot1hash  43207  omabs2  43345  clcnvlem  43636  cnvtrcl0  43639  trrelsuperrel2dg  43684  brtrclfv2  43740  imo72b2lem1  44182  fourierdlem92  46213  vsetrec  49222
  Copyright terms: Public domain W3C validator