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

Theorem syl5eqssr 3501
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 2464 . 2  |-  A  =  B
3 syl5eqssr.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3syl5eqss 3500 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1370    C_ wss 3428
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2437  df-cleq 2443  df-clel 2446  df-in 3435  df-ss 3442
This theorem is referenced by:  relcnvtr  5457  fimacnvdisj  5689  dffv2  5865  fimacnv  5936  f1ompt  5966  fnwelem  6789  tfrlem15  6953  omxpenlem  7514  hartogslem1  7859  infxpidm2  8286  alephgeom  8355  infenaleph  8364  cfflb  8531  pwfseqlem5  8933  imasvscafn  14579  mrieqvlemd  14671  cnvps  15486  dirdm  15508  tsrdir  15512  frmdss2  15645  iinopn  18633  neitr  18902  xkococnlem  19350  tgpconcomp  19801  trcfilu  19987  mbfconstlem  21225  itg2seq  21338  limcdif  21469  dvres2lem  21503  c1lip3  21589  lhop  21606  plyeq0  21797  dchrghm  22713  chssoc  25036  hauseqcn  26461  cvmliftmolem1  27306  cvmlift2lem9a  27328  cvmlift2lem9  27336  cnres2  28802  rngunsnply  29670  proot1hash  29708
  Copyright terms: Public domain W3C validator