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

Theorem syl5eqssr 3534
Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)
Hypotheses
Ref Expression
syl5eqssr.1  |-  B  =  A
syl5eqssr.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
syl5eqssr  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl5eqssr
StepHypRef Expression
1 syl5eqssr.1 . . 3  |-  B  =  A
21eqcomi 2467 . 2  |-  A  =  B
3 syl5eqssr.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3syl5eqss 3533 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1398    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  relcnvtr  5510  fimacnvdisj  5745  dffv2  5921  fimacnv  5995  f1ompt  6029  fnwelem  6888  tfrlem15  7053  omxpenlem  7611  hartogslem1  7959  infxpidm2  8385  alephgeom  8454  infenaleph  8463  cfflb  8630  pwfseqlem5  9030  imasvscafn  15026  mrieqvlemd  15118  cnvps  16041  dirdm  16063  tsrdir  16067  frmdss2  16230  iinopn  19578  neitr  19848  xkococnlem  20326  tgpconcomp  20777  trcfilu  20963  mbfconstlem  22202  itg2seq  22315  limcdif  22446  dvres2lem  22480  c1lip3  22566  lhop  22583  plyeq0  22774  dchrghm  23729  chssoc  26612  hauseqcn  28112  carsgclctunlem3  28528  cvmliftmolem1  28990  cvmlift2lem9a  29012  cvmlift2lem9  29020  cnres2  30499  rngunsnply  31363  proot1hash  31401  fourierdlem92  32220
  Copyright terms: Public domain W3C validator