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

Theorem syl5ss 3578
Description: Subclass transitivity deduction. (Contributed by NM, 6-Feb-2014.)
Hypotheses
Ref Expression
syl5ss.1 𝐴𝐵
syl5ss.2 (𝜑𝐵𝐶)
Assertion
Ref Expression
syl5ss (𝜑𝐴𝐶)

Proof of Theorem syl5ss
StepHypRef Expression
1 syl5ss.1 . . 3 𝐴𝐵
21a1i 11 . 2 (𝜑𝐴𝐵)
3 syl5ss.2 . 2 (𝜑𝐵𝐶)
42, 3sstrd 3577 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-in 3546  df-ss 3553
This theorem is referenced by:  wereu2  5025  sofld  5486  fvmptss  6186  fimacnv  6240  isofr2  6472  frxp  7151  fnse  7158  smores2  7315  f1imaen2g  7880  domunsncan  7922  dffi3  8197  marypha1lem  8199  ordtypelem7  8289  ordtypelem8  8290  oismo  8305  unxpwdom2  8353  cantnfres  8434  oemapvali  8441  tskwe  8636  acndom2  8737  dfac2a  8812  dfac12lem2  8826  cfle  8936  cofsmo  8951  coftr  8955  isf34lem5  9060  isf34lem7  9061  isf34lem6  9062  enfin1ai  9066  fin1a2lem12  9093  ttukeylem7  9197  alephexp1  9257  fpwwe2lem13  9320  fpwwe2  9321  canth4  9325  canthwelem  9328  pwfseqlem1  9336  pwfseqlem4  9340  fzossnn0  12323  fsuppmapnn0fiublem  12606  fsuppmapnn0fiub  12607  fsuppmapnn0fiubOLD  12608  xptrrel  13513  limsupgle  14002  limsupgre  14006  rlimres  14083  lo1res  14084  lo1resb  14089  rlimresb  14090  o1resb  14091  o1of2  14137  o1rlimmul  14143  isercolllem2  14190  isercoll  14192  climsup  14194  fprodntriv  14457  bitsinvp1  14955  sadcaddlem  14963  sadadd2lem  14965  sadadd3  14967  sadasslem  14976  sadeq  14978  bitsres  14979  smuval2  14988  smupval  14994  smueqlem  14996  smumul  14999  1arith  15415  isstruct2  15650  setscom  15677  ressress  15711  imasvscafn  15966  imasless  15969  mrcssv  16043  isacs1i  16087  mreacs  16088  acsfn  16089  isacs4lem  16937  isacs5lem  16938  mhmima  17132  cntzmhm  17540  f1omvdconj  17635  f1omvdco2  17637  symgsssg  17656  symggen  17659  psgnunilem1  17682  efgval  17899  gsumzaddlem  18090  gsumconst  18103  dmdprdd  18167  dprdfeq0  18190  dprdres  18196  dprdss  18197  dprdz  18198  subgdmdprd  18202  dprddisj2  18207  dprd2dlem1  18209  dprd2da  18210  dprd2d2  18212  dmdprdsplit2lem  18213  lmhmlsp  18816  lsppratlem4  18917  islbs3  18922  lbsextlem3  18927  mplcoe5  19235  mplind  19269  znleval  19667  evpmss  19696  frlmsslsp  19896  lindff1  19920  lindfrn  19921  f1lindf  19922  lindfmm  19927  lsslindf  19930  basdif0  20510  tgcl  20526  ppttop  20563  epttop  20565  ntrin  20617  mretopd  20648  neiptoptop  20687  cnclsi  20828  cnconst2  20839  cnrest2  20842  cnpresti  20844  cnprest2  20846  fiuncmp  20959  connsub  20976  conima  20980  iunconlem  20982  1stcfb  21000  2ndc1stc  21006  2ndcdisj  21011  kgentopon  21093  llycmpkgen2  21105  1stckgenlem  21108  kgencn3  21113  ptclsg  21170  ptcnplem  21176  txtube  21195  hausdiag  21200  txkgen  21207  xkoco1cn  21212  xkoco2cn  21213  xkococnlem  21214  qtoptop2  21254  basqtop  21266  imastopn  21275  hmeores  21326  hmphdis  21351  ptcmpfi  21368  fbssfi  21393  filin  21410  infil  21419  fbasrn  21440  fgtr  21446  elfm  21503  imaelfm  21507  hausflim  21537  flimclslem  21540  fclscmp  21586  cnextcn  21623  tmdgsum2  21652  tgpconcomp  21668  ustexsym  21771  ustund  21777  ustimasn  21784  utoptop  21790  utopbas  21791  restutopopn  21794  blin2  21985  metustexhalf  22112  icccmplem2  22366  icccmplem3  22367  reconnlem2  22370  tchcph  22765  fmcfil  22796  resscdrg  22879  ivthlem2  22945  ivthlem3  22946  ivth2  22948  ovolfiniun  22993  ovoliunlem1  22994  ismbl2  23019  nulmbl2  23028  unmbl  23029  shftmbl  23030  voliunlem1  23042  voliunlem2  23043  ioombl1lem4  23053  uniioombllem4  23077  dyadmbllem  23090  dyadmbl  23091  mbflimsup  23156  i1fima  23168  i1fima2  23169  i1fadd  23185  itg1addlem4  23189  itg2splitlem  23238  itg2split  23239  ellimc3  23366  limcflflem  23367  limcflf  23368  limcresi  23372  limciun  23381  dvreslem  23396  dvres2lem  23397  dvres  23398  dvaddbr  23424  dvmulbr  23425  dvlip  23477  dvlip2  23479  c1liplem1  23480  dvivthlem1  23492  dvne0  23495  lhop1lem  23497  lhop  23500  dvcnvrelem1  23501  dvcnvrelem2  23502  dvfsumle  23505  dvfsumabs  23507  dvfsumlem2  23511  itgsubstlem  23532  mdegleb  23545  mdeglt  23546  mdegldg  23547  mdegxrcl  23548  mdegcl  23550  ig1peu  23652  reeff1olem  23921  logccv  24126  rlimcnp2  24410  lgamgulmlem2  24473  ppisval  24547  prmdvdsfi  24550  mumul  24624  sqff1o  24625  chtlepsi  24648  chpub  24662  dchrisum0lem2a  24923  pntlem3  25015  ex-res  26456  htthlem  26964  chlejb1i  27525  ssmd2  28361  fimarab  28631  gsumle  28916  locfinreflem  29041  sibfof  29535  sitgclbn  29538  sitgaddlemb  29543  eulerpartlemgu  29572  ballotlemsima  29710  bnj1311  30152  erdsze2lem2  30246  iccllyscon  30292  cvmopnlem  30320  msrf  30499  nodenselem6  30891  nofulllem5  30911  neiin  31303  neibastop1  31330  neibastop2lem  31331  topmeet  31335  poimirlem1  32383  poimirlem2  32384  poimirlem3  32385  poimirlem11  32393  poimirlem12  32394  poimirlem16  32398  poimirlem19  32401  poimirlem30  32412  cnambfre  32431  itg2gt0cn  32438  sstotbnd2  32546  sstotbnd3  32548  ssbnd  32560  ismtyima  32575  heibor1lem  32581  pmodlem2  33954  pmodN  33957  diaintclN  35168  djaclN  35246  dibintclN  35277  dicval  35286  dihoml4c  35486  djhcl  35510  isnacs2  36090  isnacs3  36094  diophrw  36143  pellfundre  36266  pellfundge  36267  pellfundlb  36269  pellfundglb  36270  fnwe2lem2  36442  lmhmfgima  36475  hbt  36522  cnvtrcl0  36755  trclrelexplem  36825  relexp0a  36830  rp-imass  36888  isotone2  37170  climinf  38477  islptre  38490  limccog  38491  limcleqr  38515  itgcoscmulx  38665  ismbl3  38683  ismbl4  38690  stoweidlem27  38724  dirkercncflem2  38801  fourierdlem38  38842  fourierdlem49  38852  fourierdlem51  38854  fourierdlem54  38857  fourierdlem63  38866  fourierdlem68  38871  fourierdlem69  38872  fourierdlem70  38873  fourierdlem74  38877  fourierdlem75  38878  fourierdlem76  38879  fourierdlem80  38883  fourierdlem84  38887  fourierdlem85  38888  fourierdlem88  38891  fourierdlem100  38903  fourierdlem101  38904  fourierdlem104  38907  fourierdlem107  38910  fourierdlem111  38914  fourierdlem112  38915  caragenel2d  39226  hoidmv1lelem3  39287  hspmbllem3  39322  sssmf  39429  smfrec  39478  av-extwwlkfablem2  41512  mgmhmima  41594
  Copyright terms: Public domain W3C validator