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

Theorem syl5sseqr 3616
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 3604 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  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 2033  ax-13 2233  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:  unissint  4430  resdif  6055  fimacnv  6240  tfrlem5  7340  domss2  7981  dffi3  8197  cantnfp1lem3  8437  trcl  8464  tcid  8475  r1ordg  8501  r1sssuc  8506  ackbij1lem15  8916  cfsmolem  8952  isfin4-3  8997  fin1a2lem7  9088  wunex2  9416  wuncid  9421  trclfvlb  13543  rtrclreclem1  13592  fsumsplit  14264  o1fsum  14332  fprodsplit  14481  phimullem  15268  vdwlem6  15474  ressinbas  15709  mrcssid  16046  mreexexlem2d  16074  acsfiindd  16946  dirge  17006  symgbasfi  17575  efgredlemf  17923  efgredlemd  17926  gsumzres  18079  gsumzcl2  18080  gsumzf1o  18082  gsumadd  18092  gsumzsplit  18096  gsumsplit2  18098  dprd2da  18210  dmdprdsplit2lem  18213  dmdprdsplit2  18214  dmdprdsplit  18215  dprdsplit  18216  invrpropd  18467  issubdrg  18574  lspssid  18752  aspssid  19100  pjcss  19821  istopon  20482  sscls  20612  ordtbas  20748  cncls2  20829  tgcmp  20956  cmpfi  20963  1stcfb  21000  1stckgenlem  21108  ptbasfi  21136  ptcnplem  21176  ptuncnv  21362  ptunhmeo  21363  fbasrn  21440  cnflf2  21559  fclscmp  21586  alexsublem  21600  ghmcnp  21670  tsmsgsum  21694  tsmsres  21699  tsmssplit  21707  tsmsxplem1  21708  ustssco  21770  mopnfss  21999  cnmpt2pc  22466  uniiccdif  23069  uniioombllem3  23076  uniioombllem4  23077  itg2splitlem  23238  itg2split  23239  itgsplit  23325  ellimc2  23364  ellimc3  23366  lhop  23500  plyaddlem1  23690  plymullem1  23691  taylthlem2  23849  mtest  23879  xrlimcnp  24412  fsumharmonic  24455  chtdif  24601  dchrghm  24698  lgsquadlem2  24823  dchrisumlema  24894  dchrisumlem2  24896  dchrisum0lem1b  24921  dchrisum0lem1  24922  pntrlog2bndlem6  24989  pntlemf  25011  ex-res  26456  spanss2  27394  mdsymi  28460  padct  28691  ordtconlem1  29104  issgon  29319  sssigagen  29341  measiuns  29413  sitgclg  29537  cvmliftlem10  30336  ftc1anclem6  32456  heibor1lem  32574  heibor  32586  divrngcl  32722  isdrngo2  32723  igenss  32827  paddunssN  33908  sspadd1  33915  sspadd2  33916  pclssidN  33995  diassdvaN  35163  dochvalr  35460  lcdvbase  35696  nacsfix  36089  isnumbasgrplem2  36489  rgspnssid  36555  itgpowd  36615  trrelsuperrel2dg  36778  fvilbd  36796  relexp0a  36823  wnefimgd  37276  icccncfext  38570  iblsplit  38655  dirkeritg  38792  dirkercncflem2  38794  fourierdlem81  38877  fourierdlem89  38885  fourierdlem91  38887  fourierdlem92  38888  fourierdlem111  38907  fouriercn  38922  hspdifhsp  39303  umgr2adedgwlk  41147  umgr2adedgwlkon  41148  umgr2adedgspth  41150  srhmsubc  41863  srhmsubcALTV  41882  gsumsplit2f  41931  fdivmpt  42127  fdivpm  42130  refdivpm  42131
  Copyright terms: Public domain W3C validator