MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5eqssr Unicode version

Theorem syl5eqssr 3548
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
syl5eqssr.1
syl5eqssr.2
Assertion
Ref Expression
syl5eqssr

Proof of Theorem syl5eqssr
StepHypRef Expression
1 syl5eqssr.1 . . 3
21eqcomi 2470 . 2
3 syl5eqssr.2 . 2
42, 3syl5eqss 3547 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  =wceq 1395  C_wss 3475
This theorem is referenced by:  relcnvtr  5532  fimacnvdisj  5768  dffv2  5946  fimacnv  6019  f1ompt  6053  fnwelem  6915  tfrlem15  7080  omxpenlem  7638  hartogslem1  7988  infxpidm2  8415  alephgeom  8484  infenaleph  8493  cfflb  8660  pwfseqlem5  9062  imasvscafn  14934  mrieqvlemd  15026  cnvps  15842  dirdm  15864  tsrdir  15868  frmdss2  16031  iinopn  19411  neitr  19681  xkococnlem  20160  tgpconcomp  20611  trcfilu  20797  mbfconstlem  22036  itg2seq  22149  limcdif  22280  dvres2lem  22314  c1lip3  22400  lhop  22417  plyeq0  22608  dchrghm  23531  chssoc  26414  hauseqcn  27877  cvmliftmolem1  28726  cvmlift2lem9a  28748  cvmlift2lem9  28756  cnres2  30259  rngunsnply  31122  proot1hash  31160  fourierdlem92  31981
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator