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

Theorem syl5eqssr 3542
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 2473 . 2  |-  A  =  B
3 syl5eqssr.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3syl5eqss 3541 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1374    C_ wss 3469
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1961  ax-ext 2438
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1377  df-ex 1592  df-nf 1595  df-sb 1707  df-clab 2446  df-cleq 2452  df-clel 2455  df-in 3476  df-ss 3483
This theorem is referenced by:  relcnvtr  5518  fimacnvdisj  5754  dffv2  5931  fimacnv  6004  f1ompt  6034  fnwelem  6888  tfrlem15  7051  omxpenlem  7608  hartogslem1  7956  infxpidm2  8383  alephgeom  8452  infenaleph  8461  cfflb  8628  pwfseqlem5  9030  imasvscafn  14781  mrieqvlemd  14873  cnvps  15688  dirdm  15710  tsrdir  15714  frmdss2  15847  iinopn  19171  neitr  19440  xkococnlem  19888  tgpconcomp  20339  trcfilu  20525  mbfconstlem  21764  itg2seq  21877  limcdif  22008  dvres2lem  22042  c1lip3  22128  lhop  22145  plyeq0  22336  dchrghm  23252  chssoc  26076  hauseqcn  27499  cvmliftmolem1  28352  cvmlift2lem9a  28374  cvmlift2lem9  28382  cnres2  29849  rngunsnply  30716  proot1hash  30754  fourierdlem81  31443  fourierdlem92  31454
  Copyright terms: Public domain W3C validator