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

Theorem syl5ss 3500
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 3499 1  |-  ( ph  ->  A  C_  C )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-in 3468  df-ss 3475
This theorem is referenced by:  wereu2  4865  sofld  5439  fvmptss  5940  fimacnv  5995  isofr2  6215  frxp  6883  fnse  6890  smores2  7017  f1imaen2g  7569  domunsncan  7610  fissuni  7817  fipreima  7818  dffi3  7883  marypha1lem  7885  ordtypelem7  7941  ordtypelem8  7942  oismo  7957  unxpwdom2  8006  cantnfres  8087  oemapvali  8094  mapfienOLD  8129  tskwe  8322  acndom2  8426  dfac2a  8501  dfac12lem2  8515  cfle  8625  cofsmo  8640  coftr  8644  isf34lem5  8749  isf34lem7  8750  isf34lem6  8751  enfin1ai  8755  fin1a2lem12  8782  ttukeylem7  8886  alephexp1  8945  fpwwe2lem13  9009  fpwwe2  9010  canth4  9014  canthwelem  9017  pwfseqlem1  9025  pwfseqlem4  9029  fzossnn0  11833  fsuppmapnn0fiublem  12081  fsuppmapnn0fiub  12082  xptrrel  12901  limsupgle  13385  limsupgre  13389  rlimres  13466  lo1res  13467  lo1resb  13472  rlimresb  13473  o1resb  13474  o1of2  13520  o1rlimmul  13526  isercolllem2  13573  isercoll  13575  climsup  13577  fprodntriv  13834  bitsinvp1  14186  sadcaddlem  14194  sadadd2lem  14196  sadadd3  14198  sadasslem  14207  sadeq  14209  bitsres  14210  smuval2  14219  smupval  14225  smueqlem  14227  smumul  14230  1arith  14532  isstruct2  14728  setscom  14751  ressress  14784  imasvscafn  15029  imasless  15032  mrcssv  15106  isacs1i  15149  mreacs  15150  acsfn  15151  isacs4lem  16000  isacs5lem  16001  mhmima  16196  cntzmhm  16578  f1omvdconj  16673  f1omvdco2  16675  symgsssg  16694  symggen  16697  psgnunilem1  16720  efgval  16937  gsumzaddlem  17136  gsumzaddlemOLD  17138  gsumconst  17155  dmdprdd  17228  dprdfeq0  17260  dprdfeq0OLD  17267  dprdres  17273  dprdss  17274  dprdz  17275  subgdmdprd  17279  dprddisj2  17285  dprddisj2OLD  17286  dprd2dlem1  17288  dprd2da  17289  dprd2d2  17291  dmdprdsplit2lem  17292  lmhmlsp  17893  lsppratlem4  17994  islbs3  17999  lbsextlem3  18004  mplcoe5  18329  mplcoe2OLD  18331  mplind  18365  znleval  18769  evpmss  18798  frlmsslsp  19001  lindff1  19025  lindfrn  19026  f1lindf  19027  lindfmm  19032  lsslindf  19035  basdif0  19624  tgcl  19641  ppttop  19678  epttop  19680  ntrin  19732  mretopd  19763  neiptoptop  19802  cnclsi  19943  cnconst2  19954  cnrest2  19957  cnpresti  19959  cnprest2  19961  fiuncmp  20074  connsub  20091  conima  20095  iunconlem  20097  1stcfb  20115  2ndc1stc  20121  2ndcdisj  20126  kgentopon  20208  llycmpkgen2  20220  1stckgenlem  20223  kgencn3  20228  ptclsg  20285  ptcnplem  20291  txtube  20310  hausdiag  20315  txkgen  20322  xkoco1cn  20327  xkoco2cn  20328  xkococnlem  20329  qtoptop2  20369  basqtop  20381  imastopn  20390  hmeores  20441  hmphdis  20466  ptcmpfi  20483  fbssfi  20507  filin  20524  infil  20533  fbasrn  20554  fgtr  20560  elfm  20617  imaelfm  20621  hausflim  20651  flimclslem  20654  fclscmp  20700  cnextcn  20736  tmdgsum2  20764  tgpconcomp  20780  tsmsresOLD  20814  ustexsym  20887  ustund  20893  ustimasn  20900  utoptop  20906  utopbas  20907  restutopopn  20910  blin2  21101  metustexhalfOLD  21235  metustexhalf  21236  icccmplem2  21497  icccmplem3  21498  reconnlem2  21501  tchcph  21849  fmcfil  21880  resscdrg  21967  ivthlem2  22033  ivthlem3  22034  ivth2  22036  ovolfiniun  22081  ovoliunlem1  22082  ismbl2  22107  nulmbl2  22116  unmbl  22117  shftmbl  22118  voliunlem1  22129  voliunlem2  22130  ioombl1lem4  22140  uniioombllem4  22164  dyadmbllem  22177  dyadmbl  22178  mbflimsup  22242  i1fima  22254  i1fima2  22255  i1fadd  22271  itg1addlem4  22275  itg2splitlem  22324  itg2split  22325  ellimc3  22452  limcflflem  22453  limcflf  22454  limcresi  22458  limciun  22467  dvreslem  22482  dvres2lem  22483  dvres  22484  dvaddbr  22510  dvmulbr  22511  dvlip  22563  dvlip2  22565  c1liplem1  22566  dvivthlem1  22578  dvne0  22581  lhop1lem  22583  lhop  22586  dvcnvrelem1  22587  dvcnvrelem2  22588  dvfsumle  22591  dvfsumabs  22593  dvfsumlem2  22597  itgsubstlem  22618  mdegleb  22633  mdeglt  22634  mdegldg  22635  mdegxrcl  22636  mdegcl  22638  ig1peu  22741  reeff1olem  23010  logccv  23215  rlimcnp2  23497  ppisval  23578  prmdvdsfi  23582  mumul  23656  sqff1o  23657  chtlepsi  23682  chpub  23696  dchrisum0lem2a  23903  pntlem3  23995  ex-res  25367  ghsubgolemOLD  25573  htthlem  26035  chlejb1i  26595  ssmd2  27432  fimarab  27707  gsumle  28007  locfinreflem  28081  sibfof  28549  sitgclbn  28552  eulerpartlemgu  28583  ballotlemsima  28721  lgamgulmlem2  28839  erdsze2lem2  28915  iccllyscon  28962  cvmopnlem  28990  msrf  29169  nodenselem6  29689  nofulllem5  29709  cnambfre  30306  itg2gt0cn  30313  neiin  30393  neibastop1  30420  neibastop2lem  30421  topmeet  30425  sstotbnd2  30513  sstotbnd3  30515  ssbnd  30527  ismtyima  30542  heibor1lem  30548  isnacs2  30881  isnacs3  30885  diophrw  30934  pellfundre  31059  pellfundge  31060  pellfundlb  31062  pellfundglb  31063  fnwe2lem2  31239  lmhmfgima  31272  hbt  31323  climinf  31854  islptre  31867  limccog  31868  limcleqr  31892  itgcoscmulx  32010  stoweidlem27  32051  dirkercncflem2  32128  fourierdlem38  32169  fourierdlem49  32180  fourierdlem51  32182  fourierdlem54  32185  fourierdlem63  32194  fourierdlem68  32199  fourierdlem69  32200  fourierdlem70  32201  fourierdlem74  32205  fourierdlem75  32206  fourierdlem76  32207  fourierdlem80  32211  fourierdlem84  32215  fourierdlem85  32216  fourierdlem88  32219  fourierdlem100  32231  fourierdlem101  32232  fourierdlem104  32235  fourierdlem107  32238  fourierdlem111  32242  fourierdlem112  32243  mgmhmima  32881  bnj1311  34500  pmodlem2  35987  pmodN  35990  diaintclN  37201  djaclN  37279  dibintclN  37310  dicval  37319  dihoml4c  37519  djhcl  37543  relexp0a  38244  trclrelexplem  38250  rp-imass  38268
  Copyright terms: Public domain W3C validator