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

Theorem syl5eqssr 3634
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 2630 . 2 𝐴 = 𝐵
3 syl5eqssr.2 . 2 (𝜑𝐵𝐶)
42, 3syl5eqss 3633 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wss 3559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3566  df-ss 3573
This theorem is referenced by:  relcnvtr  5619  fimacnvdisj  6045  dffv2  6233  fimacnv  6308  f1ompt  6343  fnwelem  7244  tfrlem15  7440  omxpenlem  8013  hartogslem1  8399  infxpidm2  8792  alephgeom  8857  infenaleph  8866  cfflb  9033  pwfseqlem5  9437  imasvscafn  16129  mrieqvlemd  16221  cnvps  17144  dirdm  17166  tsrdir  17170  frmdss2  17332  iinopn  20639  neitr  20907  xkococnlem  21385  tgpconncomp  21839  trcfilu  22021  mbfconstlem  23319  itg2seq  23432  limcdif  23563  dvres2lem  23597  c1lip3  23683  lhop  23700  plyeq0  23888  dchrghm  24898  umgrres1  26111  umgr2v2e  26324  chssoc  28225  hauseqcn  29747  carsgclctunlem3  30187  cvmliftmolem1  31006  cvmlift2lem9a  31028  cvmlift2lem9  31036  cnres2  33229  rngunsnply  37259  proot1hash  37294  clcnvlem  37446  cnvtrcl0  37449  trrelsuperrel2dg  37479  brtrclfv2  37535  fourierdlem92  39748  vsetrec  41765
  Copyright terms: Public domain W3C validator