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

Theorem syl5sseqr 3240
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl5sseqr.1  |-  B  C_  A
syl5sseqr.2  |-  ( ph  ->  C  =  A )
Assertion
Ref Expression
syl5sseqr  |-  ( ph  ->  B  C_  C )

Proof of Theorem syl5sseqr
StepHypRef Expression
1 syl5sseqr.1 . . 3  |-  B  C_  A
21a1i 10 . 2  |-  ( ph  ->  B  C_  A )
3 syl5sseqr.2 . 2  |-  ( ph  ->  C  =  A )
42, 3sseqtr4d 3228 1  |-  ( ph  ->  B  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    C_ wss 3165
This theorem is referenced by:  unissint  3902  resdif  5510  fimacnv  5673  domss2  7036  dffi3  7200  cantnfp1lem3  7398  trcl  7426  tcid  7440  r1ordg  7466  r1sssuc  7471  ackbij1lem15  7876  cfsmolem  7912  isfin4-3  7957  fin1a2lem7  8048  wunex2  8376  wuncid  8381  fsumsplit  12228  o1fsum  12287  incexclem  12311  incexc  12312  phimullem  12863  vdwlem6  13049  ressinbas  13220  mrcssid  13535  mreexexlem2d  13563  acsfiindd  14296  dirge  14375  efgredlemf  15066  efgredlemd  15069  gsumzres  15210  gsumzcl  15211  gsumzf1o  15212  gsumzaddlem  15219  gsumadd  15221  gsumzsplit  15222  gsumsplit2  15224  gsumconst  15225  gsumzoppg  15232  dprd2da  15293  dmdprdsplit2lem  15296  dmdprdsplit2  15297  dmdprdsplit  15298  dprdsplit  15299  invrpropd  15496  issubdrg  15586  lspssid  15758  aspssid  16089  pjcss  16632  istopon  16679  sscls  16809  ordtbas  16938  cncls2  17018  tgcmp  17144  cmpfi  17151  1stcfb  17187  1stckgenlem  17264  ptbasfi  17292  ptcnplem  17331  ptuncnv  17514  ptunhmeo  17515  fbasrn  17595  cnflf2  17714  fclscmp  17741  alexsublem  17754  ghmcnp  17813  tsmsgsum  17837  tsmsres  17842  tsmssplit  17850  tsmsxplem1  17851  mopnfss  18005  cnmpt2pc  18442  uniiccdif  18949  uniioombllem3  18956  uniioombllem4  18957  itg2splitlem  19119  itg2split  19120  itgsplit  19206  ellimc2  19243  ellimc3  19245  lhop  19379  plyaddlem1  19611  plymullem1  19612  taylthlem2  19769  mtest  19797  xrlimcnp  20279  fsumharmonic  20321  chtdif  20412  dchrghm  20511  lgsquadlem2  20610  dchrisumlema  20653  dchrisumlem2  20655  dchrisum0lem1b  20680  dchrisum0lem1  20681  pntrlog2bndlem6  20748  pntlemf  20770  ex-res  20844  spanss2  21940  mdsymi  23007  cvmliftlem10  23840  rtrclreclem.refl  24056  rnintintrn  25229  segray  26258  heibor1lem  26636  heibor  26648  divrngcl  26691  isdrngo2  26692  igenss  26790  nacsfix  26890  isnumbasgrplem2  27372  rgspnssid  27478  paddunssN  30619  sspadd1  30626  sspadd2  30627  pclssidN  30706  diassdvaN  31872  dochvalr  32169  lcdvbase  32405
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator