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

Theorem eqsstrrid 3966
 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 2807 . 2 𝐴 = 𝐵
3 eqsstrrid.2 . 2 (𝜑𝐵𝐶)
42, 3eqsstrid 3965 1 (𝜑𝐴𝐶)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3883 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770 This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3444  df-in 3890  df-ss 3900 This theorem is referenced by:  relcnvtrg  6093  fimacnvdisj  6539  dffv2  6743  fimacnv  6826  f1ompt  6862  abnexg  7471  fnwelem  7821  tfrlem15  8029  omxpenlem  8619  hartogslem1  9008  infxpidm2  9446  alephgeom  9511  infenaleph  9520  cfflb  9688  pwfseqlem5  10092  imasvscafn  16822  mrieqvlemd  16912  cnvps  17834  dirdm  17856  tsrdir  17860  frmdss2  18040  subdrgint  19596  iinopn  21548  neitr  21826  xkococnlem  22305  tgpconncomp  22759  trcfilu  22941  mbfconstlem  24272  itg2seq  24387  limcdif  24520  dvres2lem  24554  c1lip3  24643  lhop  24660  plyeq0  24852  dchrghm  25884  uspgrupgrushgr  27014  upgrreslem  27138  umgrreslem  27139  umgrres1  27148  umgr2v2e  27359  chssoc  29323  gsumhashmul  30790  pmtrcnelor  30834  tocycfvres1  30851  tocycfvres2  30852  dimkerim  31177  hauseqcn  31317  carsgclctunlem3  31754  cvmliftmolem1  32707  cvmlift2lem9a  32729  cvmlift2lem9  32737  cnres2  35352  rngunsnply  40288  proot1hash  40315  clcnvlem  40494  cnvtrcl0  40497  trrelsuperrel2dg  40543  brtrclfv2  40599  imo72b2lem1  41045  fourierdlem92  43008  vsetrec  45398
 Copyright terms: Public domain W3C validator