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

Theorem syl5sseqr 3617
Description: Subclass transitivity deduction. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
syl5sseqr.1 𝐵𝐴
syl5sseqr.2 (𝜑𝐶 = 𝐴)
Assertion
Ref Expression
syl5sseqr (𝜑𝐵𝐶)

Proof of Theorem syl5sseqr
StepHypRef Expression
1 syl5sseqr.1 . . 3 𝐵𝐴
21a1i 11 . 2 (𝜑𝐵𝐴)
3 syl5sseqr.2 . 2 (𝜑𝐶 = 𝐴)
42, 3sseqtr4d 3605 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  wss 3540
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554
This theorem is referenced by:  unissint  4436  resdif  6070  fimacnv  6255  tfrlem5  7363  domss2  8004  dffi3  8220  cantnfp1lem3  8460  trcl  8487  tcid  8498  r1ordg  8524  r1sssuc  8529  ackbij1lem15  8939  cfsmolem  8975  isfin4-3  9020  fin1a2lem7  9111  wunex2  9439  wuncid  9444  trclfvlb  13597  rtrclreclem1  13646  fsumsplit  14318  o1fsum  14386  fprodsplit  14535  phimullem  15322  vdwlem6  15528  ressinbas  15763  mrcssid  16100  mreexexlem2d  16128  acsfiindd  17000  dirge  17060  symgbasfi  17629  efgredlemf  17977  efgredlemd  17980  gsumzres  18133  gsumzcl2  18134  gsumzf1o  18136  gsumadd  18146  gsumzsplit  18150  gsumsplit2  18152  dprd2da  18264  dmdprdsplit2lem  18267  dmdprdsplit2  18268  dmdprdsplit  18269  dprdsplit  18270  invrpropd  18521  issubdrg  18628  lspssid  18806  aspssid  19154  pjcss  19879  istopon  20540  sscls  20670  ordtbas  20806  cncls2  20887  tgcmp  21014  cmpfi  21021  1stcfb  21058  1stckgenlem  21166  ptbasfi  21194  ptcnplem  21234  ptuncnv  21420  ptunhmeo  21421  fbasrn  21498  cnflf2  21617  fclscmp  21644  alexsublem  21658  ghmcnp  21728  tsmsgsum  21752  tsmsres  21757  tsmssplit  21765  tsmsxplem1  21766  ustssco  21828  mopnfss  22058  cnmpt2pc  22535  uniiccdif  23152  uniioombllem3  23159  uniioombllem4  23160  itg2splitlem  23321  itg2split  23322  itgsplit  23408  ellimc2  23447  ellimc3  23449  lhop  23583  plyaddlem1  23773  plymullem1  23774  taylthlem2  23932  mtest  23962  xrlimcnp  24495  fsumharmonic  24538  chtdif  24684  dchrghm  24781  lgsquadlem2  24906  dchrisumlema  24977  dchrisumlem2  24979  dchrisum0lem1b  25004  dchrisum0lem1  25005  pntrlog2bndlem6  25072  pntlemf  25094  ex-res  26690  spanss2  27588  mdsymi  28654  padct  28885  ordtconlem1  29298  issgon  29513  sssigagen  29535  measiuns  29607  sitgclg  29731  cvmliftlem10  30530  ftc1anclem6  32660  heibor1lem  32778  heibor  32790  divrngcl  32926  isdrngo2  32927  igenss  33031  paddunssN  34112  sspadd1  34119  sspadd2  34120  pclssidN  34199  diassdvaN  35367  dochvalr  35664  lcdvbase  35900  nacsfix  36293  isnumbasgrplem2  36693  rgspnssid  36759  itgpowd  36819  trrelsuperrel2dg  36982  fvilbd  37000  relexp0a  37027  wnefimgd  37480  icccncfext  38773  iblsplit  38858  dirkeritg  38995  dirkercncflem2  38997  fourierdlem81  39080  fourierdlem89  39088  fourierdlem91  39090  fourierdlem92  39091  fourierdlem111  39110  fouriercn  39125  hspdifhsp  39506  umgr2adedgwlk  41152  umgr2adedgwlkon  41153  umgr2adedgspth  41155  srhmsubc  41868  srhmsubcALTV  41887  gsumsplit2f  41936  fdivmpt  42132  fdivpm  42135  refdivpm  42136  elpglem2  42254
  Copyright terms: Public domain W3C validator