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

Theorem syl5ss 3411
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 3410 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3372
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2402
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2409  df-cleq 2415  df-clel 2418  df-in 3379  df-ss 3386
This theorem is referenced by:  wereu2  4786  sofld  5239  fvmptss  5911  fimacnv  5964  isofr2  6187  frxp  6854  fnse  6861  smores2  7021  f1imaen2g  7577  domunsncan  7618  fissuni  7825  fipreima  7826  dffi3  7891  marypha1lem  7893  ordtypelem7  7985  ordtypelem8  7986  oismo  8001  unxpwdom2  8049  cantnfres  8127  oemapvali  8134  tskwe  8329  acndom2  8429  dfac2a  8504  dfac12lem2  8518  cfle  8628  cofsmo  8643  coftr  8647  isf34lem5  8752  isf34lem7  8753  isf34lem6  8754  enfin1ai  8758  fin1a2lem12  8785  ttukeylem7  8889  alephexp1  8948  fpwwe2lem13  9011  fpwwe2  9012  canth4  9016  canthwelem  9019  pwfseqlem1  9027  pwfseqlem4  9031  fzossnn0  11893  fsuppmapnn0fiublem  12145  fsuppmapnn0fiub  12146  xptrrel  12981  limsupgle  13471  limsupgre  13478  limsupgreOLD  13479  rlimres  13558  lo1res  13559  lo1resb  13564  rlimresb  13565  o1resb  13566  o1of2  13612  o1rlimmul  13618  isercolllem2  13665  isercoll  13667  climsup  13669  fprodntriv  13932  bitsinvp1  14359  sadcaddlem  14367  sadadd2lem  14369  sadadd3  14371  sadasslem  14380  sadeq  14382  bitsres  14383  smuval2  14392  smupval  14398  smueqlem  14400  smumul  14403  1arith  14807  isstruct2  15066  setscom  15089  ressress  15123  imasvscafn  15379  imasless  15382  mrcssv  15456  isacs1i  15499  mreacs  15500  acsfn  15501  isacs4lem  16350  isacs5lem  16351  mhmima  16546  cntzmhm  16928  f1omvdconj  17023  f1omvdco2  17025  symgsssg  17044  symggen  17047  psgnunilem1  17070  efgval  17303  gsumzaddlem  17490  gsumconst  17503  dmdprdd  17567  dprdfeq0  17591  dprdres  17597  dprdss  17598  dprdz  17599  subgdmdprd  17603  dprddisj2  17608  dprd2dlem1  17610  dprd2da  17611  dprd2d2  17613  dmdprdsplit2lem  17614  lmhmlsp  18208  lsppratlem4  18309  islbs3  18314  lbsextlem3  18319  mplcoe5  18628  mplind  18661  znleval  19060  evpmss  19089  frlmsslsp  19289  lindff1  19313  lindfrn  19314  f1lindf  19315  lindfmm  19320  lsslindf  19323  basdif0  19903  tgcl  19920  ppttop  19957  epttop  19959  ntrin  20011  mretopd  20043  neiptoptop  20082  cnclsi  20223  cnconst2  20234  cnrest2  20237  cnpresti  20239  cnprest2  20241  fiuncmp  20354  connsub  20371  conima  20375  iunconlem  20377  1stcfb  20395  2ndc1stc  20401  2ndcdisj  20406  kgentopon  20488  llycmpkgen2  20500  1stckgenlem  20503  kgencn3  20508  ptclsg  20565  ptcnplem  20571  txtube  20590  hausdiag  20595  txkgen  20602  xkoco1cn  20607  xkoco2cn  20608  xkococnlem  20609  qtoptop2  20649  basqtop  20661  imastopn  20670  hmeores  20721  hmphdis  20746  ptcmpfi  20763  fbssfi  20787  filin  20804  infil  20813  fbasrn  20834  fgtr  20840  elfm  20897  imaelfm  20901  hausflim  20931  flimclslem  20934  fclscmp  20980  cnextcn  21017  tmdgsum2  21046  tgpconcomp  21062  ustexsym  21165  ustund  21171  ustimasn  21178  utoptop  21184  utopbas  21185  restutopopn  21188  blin2  21379  metustexhalf  21506  icccmplem2  21776  icccmplem3  21777  reconnlem2  21780  tchcph  22146  fmcfil  22177  resscdrg  22260  ivthlem2  22338  ivthlem3  22339  ivth2  22341  ovolfiniun  22389  ovoliunlem1  22390  ismbl2  22416  nulmbl2  22425  unmbl  22426  shftmbl  22427  voliunlem1  22438  voliunlem2  22439  ioombl1lem4  22449  uniioombllem4  22479  dyadmbllem  22492  dyadmbl  22493  mbflimsup  22558  mbflimsupOLD  22559  i1fima  22571  i1fima2  22572  i1fadd  22588  itg1addlem4  22592  itg2splitlem  22641  itg2split  22642  ellimc3  22769  limcflflem  22770  limcflf  22771  limcresi  22775  limciun  22784  dvreslem  22799  dvres2lem  22800  dvres  22801  dvaddbr  22827  dvmulbr  22828  dvlip  22880  dvlip2  22882  c1liplem1  22883  dvivthlem1  22895  dvne0  22898  lhop1lem  22900  lhop  22903  dvcnvrelem1  22904  dvcnvrelem2  22905  dvfsumle  22908  dvfsumabs  22910  dvfsumlem2  22914  itgsubstlem  22935  mdegleb  22948  mdeglt  22949  mdegldg  22950  mdegxrcl  22951  mdegcl  22953  ig1peu  23057  ig1peuOLD  23058  reeff1olem  23336  logccv  23543  rlimcnp2  23827  lgamgulmlem2  23890  ppisval  23965  prmdvdsfi  23969  mumul  24043  sqff1o  24044  chtlepsi  24069  chpub  24083  dchrisum0lem2a  24290  pntlem3  24382  ex-res  25826  ghsubgolemOLD  26033  htthlem  26505  chlejb1i  27064  ssmd2  27900  fimarab  28183  gsumle  28486  locfinreflem  28612  sibfof  29118  sitgclbn  29121  sitgaddlemb  29126  eulerpartlemgu  29155  ballotlemsima  29293  ballotlemsimaOLD  29331  bnj1311  29778  erdsze2lem2  29872  iccllyscon  29918  cvmopnlem  29946  msrf  30125  nodenselem6  30517  nofulllem5  30537  neiin  30930  neibastop1  30957  neibastop2lem  30958  topmeet  30962  poimirlem1  31842  poimirlem2  31843  poimirlem3  31844  poimirlem11  31852  poimirlem12  31853  poimirlem16  31857  poimirlem19  31860  poimirlem30  31871  cnambfre  31890  itg2gt0cn  31898  sstotbnd2  32007  sstotbnd3  32009  ssbnd  32021  ismtyima  32036  heibor1lem  32042  pmodlem2  33318  pmodN  33321  diaintclN  34532  djaclN  34610  dibintclN  34641  dicval  34650  dihoml4c  34850  djhcl  34874  isnacs2  35454  isnacs3  35458  diophrw  35507  pellfundre  35636  pellfundge  35637  pellfundlb  35639  pellfundglb  35640  fnwe2lem2  35816  lmhmfgima  35849  hbt  35896  cnvtrcl0  36140  trclrelexplem  36210  relexp0a  36215  rp-imass  36273  climinf  37561  climinfOLD  37562  islptre  37576  limccog  37577  limcleqr  37602  itgcoscmulx  37723  stoweidlem27  37764  dirkercncflem2  37843  fourierdlem38  37885  fourierdlem49  37896  fourierdlem51  37898  fourierdlem54  37901  fourierdlem63  37910  fourierdlem68  37915  fourierdlem69  37916  fourierdlem70  37917  fourierdlem74  37921  fourierdlem75  37922  fourierdlem76  37923  fourierdlem80  37927  fourierdlem84  37931  fourierdlem85  37932  fourierdlem88  37935  fourierdlem100  37947  fourierdlem101  37948  fourierdlem104  37951  fourierdlem107  37954  fourierdlem111  37958  fourierdlem112  37959  hoidmv1lelem3  38256  mgmhmima  39387
  Copyright terms: Public domain W3C validator