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

Theorem syl5ss 3319
Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
Hypotheses
Ref Expression
syl5ss.1  |-  A  C_  B
syl5ss.2  |-  ( ph  ->  B  C_  C )
Assertion
Ref Expression
syl5ss  |-  ( ph  ->  A  C_  C )

Proof of Theorem syl5ss
StepHypRef Expression
1 syl5ss.1 . . 3  |-  A  C_  B
21a1i 11 . 2  |-  ( ph  ->  A  C_  B )
3 syl5ss.2 . 2  |-  ( ph  ->  B  C_  C )
42, 3sstrd 3318 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff set class
Syntax hints:    -> wi 4    C_ wss 3280
This theorem is referenced by:  wereu2  4539  sofld  5277  fvmptss  5772  fimacnv  5821  isofr2  6023  frxp  6415  fnse  6422  smores2  6575  f1imaen2g  7127  domunsncan  7167  fissuni  7369  fipreima  7370  dffi3  7394  marypha1lem  7396  ordtypelem7  7449  ordtypelem8  7450  oismo  7465  unxpwdom2  7512  oemapvali  7596  mapfien  7609  tskwe  7793  acndom2  7891  dfac2a  7966  dfac12lem2  7980  cfle  8090  cofsmo  8105  coftr  8109  isf34lem5  8214  isf34lem7  8215  isf34lem6  8216  enfin1ai  8220  fin1a2lem12  8247  ttukeylem7  8351  alephexp1  8410  fpwwe2lem13  8473  fpwwe2  8474  canth4  8478  canthwelem  8481  pwfseqlem1  8489  pwfseqlem4  8493  limsupgle  12226  limsupgre  12230  rlimres  12307  lo1res  12308  lo1resb  12313  rlimresb  12314  o1resb  12315  o1of2  12361  o1rlimmul  12367  isercolllem2  12414  isercoll  12416  climsup  12418  bitsinvp1  12916  sadcaddlem  12924  sadadd2lem  12926  sadadd3  12928  sadasslem  12937  sadeq  12939  bitsres  12940  smuval2  12949  smupval  12955  smueqlem  12957  smumul  12960  1arith  13250  isstruct2  13433  setscom  13452  ressress  13481  imasvscafn  13717  imasless  13720  mrcssv  13794  isacs1i  13837  mreacs  13838  acsfn  13839  isacs4lem  14549  isacs5lem  14550  mhmima  14718  cntzmhm  15092  efgval  15304  gsumzaddlem  15481  dmdprdd  15515  dprdfeq0  15535  dprdres  15541  dprdss  15542  dprdz  15543  subgdmdprd  15547  dprddisj2  15552  dprd2dlem1  15554  dprd2da  15555  dprd2d2  15557  dmdprdsplit2lem  15558  lmhmlsp  16080  lsppratlem4  16177  islbs3  16182  lbsextlem3  16187  mplcoe2  16485  mplind  16517  znleval  16790  basdif0  16973  tgcl  16989  ppttop  17026  epttop  17028  ntrin  17080  mretopd  17111  neiptoptop  17150  cnclsi  17290  cnconst2  17301  cnrest  17303  cnrest2  17304  cnpresti  17306  cnprest2  17308  fiuncmp  17421  connsub  17437  conima  17441  iunconlem  17443  1stcfb  17461  2ndc1stc  17467  2ndcdisj  17472  kgentopon  17523  llycmpkgen2  17535  1stckgenlem  17538  kgencn3  17543  ptclsg  17600  ptcnplem  17606  txtube  17625  hausdiag  17630  txkgen  17637  xkoco1cn  17642  xkoco2cn  17643  xkococnlem  17644  qtoptop2  17684  basqtop  17696  imastopn  17705  hmeores  17756  hmphdis  17781  ptcmpfi  17798  fbssfi  17822  filin  17839  infil  17848  fbasrn  17869  fgtr  17875  elfm  17932  imaelfm  17936  hausflim  17966  flimclslem  17969  fclscmp  18015  cnextcn  18051  tmdgsum2  18079  tgpconcomp  18095  tsmsres  18126  ustexsym  18198  ustund  18204  ustimasn  18211  utoptop  18217  utopbas  18218  restutopopn  18221  blin2  18412  metustexhalfOLD  18546  metustexhalf  18547  icccmplem2  18807  icccmplem3  18808  reconnlem2  18811  tchcph  19147  fmcfil  19178  resscdrg  19265  ivthlem2  19302  ivthlem3  19303  ivth2  19305  ovolfiniun  19350  ovoliunlem1  19351  ismbl2  19376  nulmbl2  19384  unmbl  19385  shftmbl  19386  voliunlem1  19397  voliunlem2  19398  ioombl1lem4  19408  uniioombllem4  19431  dyadmbllem  19444  dyadmbl  19445  mbflimsup  19511  i1fima  19523  i1fima2  19524  i1fadd  19540  itg1addlem4  19544  itg2splitlem  19593  itg2split  19594  ellimc3  19719  limcflflem  19720  limcflf  19721  limcresi  19725  limciun  19734  dvreslem  19749  dvres2lem  19750  dvres  19751  dvaddbr  19777  dvmulbr  19778  dvlip  19830  dvlip2  19832  c1liplem1  19833  dvivthlem1  19845  dvne0  19848  lhop1lem  19850  lhop  19853  dvcnvrelem1  19854  dvcnvrelem2  19855  dvfsumle  19858  dvfsumabs  19860  dvfsumlem2  19864  itgsubstlem  19885  mdegleb  19940  mdeglt  19941  mdegldg  19942  mdegxrcl  19943  mdegcl  19945  ig1peu  20047  reeff1olem  20315  logccv  20507  rlimcnp2  20758  ppisval  20839  prmdvdsfi  20843  mumul  20917  sqff1o  20918  chtlepsi  20943  chpub  20957  dchrisum0lem2a  21164  pntlem3  21256  ex-res  21702  ghsubgolem  21911  htthlem  22373  chlejb1i  22931  ssmd2  23768  sibfof  24607  sitgclbn  24610  ballotlemsima  24726  lgamgulmlem2  24767  erdsze2lem2  24843  iccllyscon  24890  cvmopnlem  24918  relexpdm  25088  relexprn  25089  fprodntriv  25221  nodenselem6  25554  nofulllem5  25574  cnambfre  26154  itg2gt0cn  26159  neiin  26225  neibastop1  26278  neibastop2lem  26279  topmeet  26283  sstotbnd2  26373  sstotbnd3  26375  ssbnd  26387  ismtyima  26402  heibor1lem  26408  isnacs2  26650  isnacs3  26654  diophrw  26707  pellfundre  26834  pellfundge  26835  pellfundlb  26837  pellfundglb  26838  fnwe2lem2  27016  lmhmfgima  27050  frlmsslsp  27116  lindff1  27158  lindfrn  27159  f1lindf  27160  lindfmm  27165  lsslindf  27168  hbt  27202  f1omvdconj  27257  f1omvdco2  27259  symgsssg  27276  symggen  27279  psgnunilem1  27284  climinf  27599  stoweidlem27  27643  swrdccatin12lem3c  28023  bnj1311  29099  pmodlem2  30329  pmodN  30332  diaintclN  31541  djaclN  31619  dibintclN  31650  dicval  31659  dihoml4c  31859  djhcl  31883
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-in 3287  df-ss 3294
  Copyright terms: Public domain W3C validator