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

Theorem syl5ss 3372
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 3371 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3333
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-in 3340  df-ss 3347
This theorem is referenced by:  wereu2  4722  sofld  5291  fvmptss  5787  fimacnv  5840  isofr2  6040  frxp  6687  fnse  6694  smores2  6820  f1imaen2g  7375  domunsncan  7416  fissuni  7621  fipreima  7622  dffi3  7686  marypha1lem  7688  ordtypelem7  7743  ordtypelem8  7744  oismo  7759  unxpwdom2  7808  cantnfres  7890  oemapvali  7897  mapfienOLD  7932  tskwe  8125  acndom2  8229  dfac2a  8304  dfac12lem2  8318  cfle  8428  cofsmo  8443  coftr  8447  isf34lem5  8552  isf34lem7  8553  isf34lem6  8554  enfin1ai  8558  fin1a2lem12  8585  ttukeylem7  8689  alephexp1  8748  fpwwe2lem13  8814  fpwwe2  8815  canth4  8819  canthwelem  8822  pwfseqlem1  8830  pwfseqlem4  8834  fzossnn0  11585  limsupgle  12960  limsupgre  12964  rlimres  13041  lo1res  13042  lo1resb  13047  rlimresb  13048  o1resb  13049  o1of2  13095  o1rlimmul  13101  isercolllem2  13148  isercoll  13150  climsup  13152  bitsinvp1  13650  sadcaddlem  13658  sadadd2lem  13660  sadadd3  13662  sadasslem  13671  sadeq  13673  bitsres  13674  smuval2  13683  smupval  13689  smueqlem  13691  smumul  13694  1arith  13993  isstruct2  14188  setscom  14209  ressress  14240  imasvscafn  14480  imasless  14483  mrcssv  14557  isacs1i  14600  mreacs  14601  acsfn  14602  isacs4lem  15343  isacs5lem  15344  mhmima  15496  cntzmhm  15861  f1omvdconj  15957  f1omvdco2  15959  symgsssg  15978  symggen  15981  psgnunilem1  16004  efgval  16219  gsumzaddlem  16413  gsumzaddlemOLD  16415  dmdprdd  16486  dprdfeq0  16517  dprdfeq0OLD  16524  dprdres  16530  dprdss  16531  dprdz  16532  subgdmdprd  16536  dprddisj2  16542  dprddisj2OLD  16543  dprd2dlem1  16545  dprd2da  16546  dprd2d2  16548  dmdprdsplit2lem  16549  lmhmlsp  17135  lsppratlem4  17236  islbs3  17241  lbsextlem3  17246  mplcoe5  17553  mplcoe2OLD  17555  mplind  17589  znleval  17992  evpmss  18021  frlmsslsp  18228  frlmsslspOLD  18229  lindff1  18254  lindfrn  18255  f1lindf  18256  lindfmm  18261  lsslindf  18264  basdif0  18563  tgcl  18579  ppttop  18616  epttop  18618  ntrin  18670  mretopd  18701  neiptoptop  18740  islp3  18755  cnclsi  18881  cnconst2  18892  cnrest  18894  cnrest2  18895  cnpresti  18897  cnprest2  18899  fiuncmp  19012  connsub  19030  conima  19034  iunconlem  19036  1stcfb  19054  2ndc1stc  19060  2ndcdisj  19065  kgentopon  19116  llycmpkgen2  19128  1stckgenlem  19131  kgencn3  19136  ptclsg  19193  ptcnplem  19199  txtube  19218  hausdiag  19223  txkgen  19230  xkoco1cn  19235  xkoco2cn  19236  xkococnlem  19237  qtoptop2  19277  basqtop  19289  imastopn  19298  hmeores  19349  hmphdis  19374  ptcmpfi  19391  fbssfi  19415  filin  19432  infil  19441  fbasrn  19462  fgtr  19468  elfm  19525  imaelfm  19529  hausflim  19559  flimclslem  19562  fclscmp  19608  cnextcn  19644  tmdgsum2  19672  tgpconcomp  19688  tsmsresOLD  19722  ustexsym  19795  ustund  19801  ustimasn  19808  utoptop  19814  utopbas  19815  restutopopn  19818  blin2  20009  metustexhalfOLD  20143  metustexhalf  20144  icccmplem2  20405  icccmplem3  20406  reconnlem2  20409  tchcph  20757  fmcfil  20788  resscdrg  20875  ivthlem2  20941  ivthlem3  20942  ivth2  20944  ovolfiniun  20989  ovoliunlem1  20990  ismbl2  21015  nulmbl2  21023  unmbl  21024  shftmbl  21025  voliunlem1  21036  voliunlem2  21037  ioombl1lem4  21047  uniioombllem4  21071  dyadmbllem  21084  dyadmbl  21085  mbflimsup  21149  i1fima  21161  i1fima2  21162  i1fadd  21178  itg1addlem4  21182  itg2splitlem  21231  itg2split  21232  ellimc3  21359  limcflflem  21360  limcflf  21361  limcresi  21365  limciun  21374  dvreslem  21389  dvres2lem  21390  dvres  21391  dvaddbr  21417  dvmulbr  21418  dvlip  21470  dvlip2  21472  c1liplem1  21473  dvivthlem1  21485  dvne0  21488  lhop1lem  21490  lhop  21493  dvcnvrelem1  21494  dvcnvrelem2  21495  dvfsumle  21498  dvfsumabs  21500  dvfsumlem2  21504  itgsubstlem  21525  mdegleb  21540  mdeglt  21541  mdegldg  21542  mdegxrcl  21543  mdegcl  21545  ig1peu  21648  reeff1olem  21916  logccv  22113  rlimcnp2  22365  ppisval  22446  prmdvdsfi  22450  mumul  22524  sqff1o  22525  chtlepsi  22550  chpub  22564  dchrisum0lem2a  22771  pntlem3  22863  ex-res  23653  ghsubgolem  23862  htthlem  24324  chlejb1i  24884  ssmd2  25721  gsumle  26251  gsumvsca1  26256  gsumvsca2  26257  sibfof  26731  sitgclbn  26734  eulerpartlemgu  26765  ballotlemsima  26903  lgamgulmlem2  27021  erdsze2lem2  27097  iccllyscon  27144  cvmopnlem  27172  relexpdm  27342  relexprn  27343  fprodntriv  27460  nodenselem6  27832  nofulllem5  27852  cnambfre  28445  itg2gt0cn  28452  neiin  28532  neibastop1  28585  neibastop2lem  28586  topmeet  28590  sstotbnd2  28678  sstotbnd3  28680  ssbnd  28692  ismtyima  28707  heibor1lem  28713  isnacs2  29047  isnacs3  29051  diophrw  29102  pellfundre  29227  pellfundge  29228  pellfundlb  29230  pellfundglb  29231  fnwe2lem2  29409  lmhmfgima  29442  hbt  29491  climinf  29784  stoweidlem27  29827  fsuppmapnn0fiublem  30803  fsuppmapnn0fiub  30804  bnj1311  32020  pmodlem2  33496  pmodN  33499  diaintclN  34708  djaclN  34786  dibintclN  34817  dicval  34826  dihoml4c  35026  djhcl  35050
  Copyright terms: Public domain W3C validator