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

Theorem syl5eqssr 3799
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 2780 . 2 𝐴 = 𝐵
3 syl5eqssr.2 . 2 (𝜑𝐵𝐶)
42, 3syl5eqss 3798 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1631  wss 3723
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-ext 2751
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-in 3730  df-ss 3737
This theorem is referenced by:  relcnvtr  5799  fimacnvdisj  6223  dffv2  6413  fimacnv  6490  f1ompt  6524  abnexg  7111  fnwelem  7443  tfrlem15  7641  omxpenlem  8217  hartogslem1  8603  infxpidm2  9040  alephgeom  9105  infenaleph  9114  cfflb  9283  pwfseqlem5  9687  imasvscafn  16405  mrieqvlemd  16497  cnvps  17420  dirdm  17442  tsrdir  17446  frmdss2  17608  iinopn  20927  neitr  21205  xkococnlem  21683  tgpconncomp  22136  trcfilu  22318  mbfconstlem  23615  itg2seq  23729  limcdif  23860  dvres2lem  23894  c1lip3  23982  lhop  23999  plyeq0  24187  dchrghm  25202  uspgrupgrushgr  26294  upgrreslem  26419  umgrreslem  26420  umgrres1  26429  umgr2v2e  26656  chssoc  28695  hauseqcn  30281  carsgclctunlem3  30722  cvmliftmolem1  31601  cvmlift2lem9a  31623  cvmlift2lem9  31631  cnres2  33894  rngunsnply  38269  proot1hash  38304  clcnvlem  38456  cnvtrcl0  38459  trrelsuperrel2dg  38489  brtrclfv2  38545  fourierdlem92  40932  vsetrec  42977
  Copyright terms: Public domain W3C validator