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

Theorem syl5ss 3647
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 3646 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  wereu2  5140  sofld  5616  fvmptss  6331  fimacnv  6387  isofr2  6634  frxp  7332  fnse  7339  smores2  7496  f1imaen2g  8058  domunsncan  8101  dffi3  8378  marypha1lem  8380  ordtypelem7  8470  ordtypelem8  8471  oismo  8486  unxpwdom2  8534  cantnfres  8612  oemapvali  8619  tskwe  8814  acndom2  8915  dfac2a  8990  dfac12lem2  9004  cfle  9114  cofsmo  9129  coftr  9133  isf34lem5  9238  isf34lem7  9239  isf34lem6  9240  enfin1ai  9244  fin1a2lem12  9271  ttukeylem7  9375  alephexp1  9439  fpwwe2lem13  9502  fpwwe2  9503  canth4  9507  canthwelem  9510  pwfseqlem1  9518  pwfseqlem4  9522  fzossnn0  12538  fsuppmapnn0fiublem  12829  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  xptrrel  13765  limsupgle  14252  limsupgre  14256  rlimres  14333  lo1res  14334  lo1resb  14339  rlimresb  14340  o1resb  14341  o1of2  14387  o1rlimmul  14393  isercolllem2  14440  isercoll  14442  climsup  14444  fprodntriv  14716  bitsinvp1  15218  sadcaddlem  15226  sadadd2lem  15228  sadadd3  15230  sadasslem  15239  sadeq  15241  bitsres  15242  smuval2  15251  smupval  15257  smueqlem  15259  smumul  15262  1arith  15678  isstruct2  15914  setscom  15950  ressress  15985  imasvscafn  16244  imasless  16247  mrcssv  16321  isacs1i  16365  mreacs  16366  acsfn  16367  isacs4lem  17215  isacs5lem  17216  mhmima  17410  cntzmhm  17817  f1omvdconj  17912  f1omvdco2  17914  symgsssg  17933  symggen  17936  psgnunilem1  17959  efgval  18176  gsumzaddlem  18367  gsumconst  18380  dmdprdd  18444  dprdfeq0  18467  dprdres  18473  dprdss  18474  dprdz  18475  subgdmdprd  18479  dprddisj2  18484  dprd2dlem1  18486  dprd2da  18487  dprd2d2  18489  dmdprdsplit2lem  18490  lmhmlsp  19097  lsppratlem4  19198  islbs3  19203  lbsextlem3  19208  mplcoe5  19516  mplind  19550  znleval  19951  evpmss  19980  frlmsslsp  20183  lindff1  20207  lindfrn  20208  f1lindf  20209  lindfmm  20214  lsslindf  20217  basdif0  20805  tgcl  20821  ppttop  20859  epttop  20861  ntrin  20913  mretopd  20944  neiptoptop  20983  cnclsi  21124  cnconst2  21135  cnrest2  21138  cnpresti  21140  cnprest2  21142  fiuncmp  21255  connsub  21272  connima  21276  iunconnlem  21278  1stcfb  21296  2ndc1stc  21302  2ndcdisj  21307  kgentopon  21389  llycmpkgen2  21401  1stckgenlem  21404  kgencn3  21409  ptclsg  21466  ptcnplem  21472  txtube  21491  hausdiag  21496  txkgen  21503  xkoco1cn  21508  xkoco2cn  21509  xkococnlem  21510  qtoptop2  21550  basqtop  21562  imastopn  21571  hmeores  21622  hmphdis  21647  ptcmpfi  21664  fbssfi  21688  filin  21705  infil  21714  fbasrn  21735  fgtr  21741  elfm  21798  imaelfm  21802  hausflim  21832  flimclslem  21835  fclscmp  21881  cnextcn  21918  tmdgsum2  21947  tgpconncomp  21963  ustexsym  22066  ustund  22072  ustimasn  22079  utoptop  22085  utopbas  22086  restutopopn  22089  blin2  22281  metustexhalf  22408  icccmplem2  22673  icccmplem3  22674  reconnlem2  22677  tchcph  23082  fmcfil  23116  resscdrg  23200  ivthlem2  23267  ivthlem3  23268  ivth2  23270  ovolfiniun  23315  ovoliunlem1  23316  ismbl2  23341  nulmbl2  23350  unmbl  23351  shftmbl  23352  voliunlem1  23364  voliunlem2  23365  ioombl1lem4  23375  uniioombllem4  23400  dyadmbllem  23413  dyadmbl  23414  mbflimsup  23478  i1fima  23490  i1fima2  23491  i1fadd  23507  itg1addlem4  23511  itg2splitlem  23560  itg2split  23561  ellimc3  23688  limcflflem  23689  limcflf  23690  limcresi  23694  limciun  23703  dvreslem  23718  dvres2lem  23719  dvres  23720  dvaddbr  23746  dvmulbr  23747  dvlip  23801  dvlip2  23803  c1liplem1  23804  dvivthlem1  23816  dvne0  23819  lhop1lem  23821  lhop  23824  dvcnvrelem1  23825  dvcnvrelem2  23826  dvfsumle  23829  dvfsumabs  23831  dvfsumlem2  23835  itgsubstlem  23856  mdegleb  23869  mdeglt  23870  mdegldg  23871  mdegxrcl  23872  mdegcl  23874  ig1peu  23976  reeff1olem  24245  logccv  24454  rlimcnp2  24738  lgamgulmlem2  24801  ppisval  24875  prmdvdsfi  24878  mumul  24952  sqff1o  24953  chtlepsi  24976  chpub  24990  dchrisum0lem2a  25251  pntlem3  25343  ex-res  27428  htthlem  27902  chlejb1i  28463  ssmd2  29299  fimarab  29573  fz2ssnn0  29675  gsumle  29907  locfinreflem  30035  sibfof  30530  sitgclbn  30533  sitgaddlemb  30538  eulerpartlemgu  30567  ballotlemsima  30705  reprinrn  30824  bnj1311  31218  erdsze2lem2  31312  iccllysconn  31358  cvmopnlem  31386  msrf  31565  frpomin  31863  frrlem4  31908  nosupno  31974  neiin  32452  neibastop1  32479  neibastop2lem  32480  topmeet  32484  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem11  33550  poimirlem12  33551  poimirlem16  33555  poimirlem19  33558  poimirlem30  33569  cnambfre  33588  itg2gt0cn  33595  sstotbnd2  33703  sstotbnd3  33705  ssbnd  33717  ismtyima  33732  heibor1lem  33738  idresssidinxp  34220  pmodlem2  35451  pmodN  35454  diaintclN  36664  djaclN  36742  dibintclN  36773  dicval  36782  dihoml4c  36982  djhcl  37006  isnacs2  37586  isnacs3  37590  diophrw  37639  pellfundre  37762  pellfundge  37763  pellfundlb  37765  pellfundglb  37766  fnwe2lem2  37938  lmhmfgima  37971  hbt  38017  cnvtrcl0  38250  trclrelexplem  38320  relexp0a  38325  rp-imass  38382  isotone2  38664  climinf  40156  islptre  40169  limccog  40170  limcleqr  40194  itgcoscmulx  40503  ismbl3  40521  ismbl4  40528  stoweidlem27  40562  dirkercncflem2  40639  fourierdlem38  40680  fourierdlem49  40690  fourierdlem51  40692  fourierdlem54  40695  fourierdlem63  40704  fourierdlem68  40709  fourierdlem69  40710  fourierdlem70  40711  fourierdlem74  40715  fourierdlem75  40716  fourierdlem76  40717  fourierdlem80  40721  fourierdlem84  40725  fourierdlem85  40726  fourierdlem88  40729  fourierdlem100  40741  fourierdlem101  40742  fourierdlem104  40745  fourierdlem107  40748  fourierdlem111  40752  fourierdlem112  40753  caragenel2d  41067  hoidmv1lelem3  41128  hspmbllem3  41163  sssmf  41268  smfrec  41317  smfsuplem1  41338  mgmhmima  42127
  Copyright terms: Public domain W3C validator