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

Theorem eqsstrrid 3998
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 3997 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  wss 3915
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 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932
This theorem is referenced by:  relcnvtrg  6223  fimacnvdisj  6725  dffv2  6941  fimacnvOLD  7026  f1ompt  7064  abnexg  7695  fnwelem  8068  tfrlem15  8343  omxpenlem  9024  hartogslem1  9485  ttrcltr  9659  dfttrcl2  9667  infxpidm2  9960  alephgeom  10025  infenaleph  10034  cfflb  10202  pwfseqlem5  10606  imasvscafn  17426  mrieqvlemd  17516  cnvps  18474  dirdm  18496  tsrdir  18500  frmdss2  18680  subdrgint  20286  iinopn  22267  neitr  22547  xkococnlem  23026  tgpconncomp  23480  trcfilu  23662  mbfconstlem  25007  itg2seq  25123  limcdif  25256  dvres2lem  25290  c1lip3  25379  lhop  25396  plyeq0  25588  dchrghm  26620  uspgrupgrushgr  28170  upgrreslem  28294  umgrreslem  28295  umgrres1  28304  umgr2v2e  28515  chssoc  30480  gsumhashmul  31940  pmtrcnelor  31984  tocycfvres1  32001  tocycfvres2  32002  dimkerim  32362  hauseqcn  32519  carsgclctunlem3  32960  cvmliftmolem1  33915  cvmlift2lem9a  33937  cvmlift2lem9  33945  cnres2  36251  rngunsnply  41529  proot1hash  41556  omabs2  41696  clcnvlem  41969  cnvtrcl0  41972  trrelsuperrel2dg  42017  brtrclfv2  42073  imo72b2lem1  42516  fourierdlem92  44513  vsetrec  47222
  Copyright terms: Public domain W3C validator