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

Theorem syl5eqssr 3683
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 2660 . 2 𝐴 = 𝐵
3 syl5eqssr.2 . 2 (𝜑𝐵𝐶)
42, 3syl5eqss 3682 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  relcnvtr  5693  fimacnvdisj  6121  dffv2  6310  fimacnv  6387  f1ompt  6422  abnexg  7006  fnwelem  7337  tfrlem15  7533  omxpenlem  8102  hartogslem1  8488  infxpidm2  8878  alephgeom  8943  infenaleph  8952  cfflb  9119  pwfseqlem5  9523  imasvscafn  16244  mrieqvlemd  16336  cnvps  17259  dirdm  17281  tsrdir  17285  frmdss2  17447  iinopn  20755  neitr  21032  xkococnlem  21510  tgpconncomp  21963  trcfilu  22145  mbfconstlem  23441  itg2seq  23554  limcdif  23685  dvres2lem  23719  c1lip3  23807  lhop  23824  plyeq0  24012  dchrghm  25026  uspgrupgrushgr  26117  upgrreslem  26241  umgrreslem  26242  umgrres1  26251  umgr2v2e  26477  chssoc  28483  hauseqcn  30069  carsgclctunlem3  30510  cvmliftmolem1  31389  cvmlift2lem9a  31411  cvmlift2lem9  31419  cnres2  33692  rngunsnply  38060  proot1hash  38095  clcnvlem  38247  cnvtrcl0  38250  trrelsuperrel2dg  38280  brtrclfv2  38336  fourierdlem92  40733  vsetrec  42774
  Copyright terms: Public domain W3C validator