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

Theorem syl5eqssr 3444
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 2460 . 2  |-  A  =  B
3 syl5eqssr.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3syl5eqss 3443 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1447    C_ wss 3371
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1672  ax-4 1685  ax-5 1761  ax-6 1808  ax-7 1854  ax-10 1918  ax-11 1923  ax-12 1936  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1450  df-ex 1667  df-nf 1671  df-sb 1801  df-clab 2438  df-cleq 2444  df-clel 2447  df-in 3378  df-ss 3385
This theorem is referenced by:  relcnvtr  5333  fimacnvdisj  5743  dffv2  5921  fimacnv  5995  f1ompt  6027  fnwelem  6898  tfrlem15  7096  omxpenlem  7659  hartogslem1  8043  infxpidm2  8434  alephgeom  8499  infenaleph  8508  cfflb  8675  pwfseqlem5  9074  imasvscafn  15453  mrieqvlemd  15545  cnvps  16468  dirdm  16490  tsrdir  16494  frmdss2  16657  iinopn  19942  neitr  20206  xkococnlem  20684  tgpconcomp  21137  trcfilu  21319  mbfconstlem  22596  itg2seq  22711  limcdif  22842  dvres2lem  22876  c1lip3  22962  lhop  22979  plyeq0  23176  dchrghm  24195  chssoc  27160  hauseqcn  28707  carsgclctunlem3  29157  cvmliftmolem1  30009  cvmlift2lem9a  30031  cvmlift2lem9  30039  cnres2  32096  rngunsnply  36040  proot1hash  36078  clcnvlem  36231  cnvtrcl0  36234  trrelsuperrel2dg  36264  brtrclfv2  36320  fourierdlem92  38118  umgrres1  39482  umgr2v2e  39663
  Copyright terms: Public domain W3C validator