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

Theorem syl5sseqr 3795
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 3783 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wss 3715
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-in 3722  df-ss 3729
This theorem is referenced by:  unissint  4653  resdif  6318  fimacnv  6510  tfrlem5  7645  domss2  8284  dffi3  8502  cantnfp1lem3  8750  trcl  8777  tcid  8788  r1ordg  8814  r1sssuc  8819  ackbij1lem15  9248  cfsmolem  9284  isfin4-3  9329  fin1a2lem7  9420  wunex2  9752  wuncid  9757  trclfvlb  13948  rtrclreclem1  13997  fsumsplit  14670  o1fsum  14744  fprodsplit  14895  phimullem  15686  vdwlem6  15892  ressinbas  16138  mrcssid  16479  mreexexlem2d  16507  acsfiindd  17378  dirge  17438  symgbasfi  18006  efgredlemf  18354  efgredlemd  18357  gsumzres  18510  gsumzcl2  18511  gsumzf1o  18513  gsumadd  18523  gsumzsplit  18527  gsumsplit2  18529  dprd2da  18641  dmdprdsplit2lem  18644  dmdprdsplit2  18645  dmdprdsplit  18646  dprdsplit  18647  invrpropd  18898  issubdrg  19007  lspssid  19187  aspssid  19535  pjcss  20262  istopon  20919  sscls  21062  ordtbas  21198  cncls2  21279  tgcmp  21406  cmpfi  21413  1stcfb  21450  1stckgenlem  21558  ptbasfi  21586  ptcnplem  21626  ptuncnv  21812  ptunhmeo  21813  fbasrn  21889  cnflf2  22008  fclscmp  22035  alexsublem  22049  ghmcnp  22119  tsmsgsum  22143  tsmsres  22148  tsmssplit  22156  tsmsxplem1  22157  ustssco  22219  mopnfss  22449  cnmpt2pc  22928  uniiccdif  23546  uniioombllem3  23553  uniioombllem4  23554  itg2splitlem  23714  itg2split  23715  itgsplit  23801  ellimc2  23840  ellimc3  23842  lhop  23978  plyaddlem1  24168  plymullem1  24169  taylthlem2  24327  mtest  24357  xrlimcnp  24894  fsumharmonic  24937  chtdif  25083  dchrghm  25180  lgsquadlem2  25305  dchrisumlema  25376  dchrisumlem2  25378  dchrisum0lem1b  25403  dchrisum0lem1  25404  pntrlog2bndlem6  25471  pntlemf  25493  nbupgruvtxres  26512  umgr2adedgwlk  27065  umgr2adedgwlkon  27066  umgr2adedgspth  27068  ex-res  27609  spanss2  28513  mdsymi  29579  padct  29806  ordtconnlem1  30279  issgon  30495  sssigagen  30517  measiuns  30589  sitgclg  30713  cvmliftlem10  31583  ftc1anclem6  33803  heibor1lem  33921  heibor  33933  divrngcl  34069  isdrngo2  34070  igenss  34174  paddunssN  35597  sspadd1  35604  sspadd2  35605  pclssidN  35684  diassdvaN  36851  dochvalr  37148  lcdvbase  37384  nacsfix  37777  isnumbasgrplem2  38176  rgspnssid  38242  itgpowd  38302  trrelsuperrel2dg  38465  fvilbd  38483  relexp0a  38510  wnefimgd  38962  icccncfext  40603  iblsplit  40685  dirkeritg  40822  dirkercncflem2  40824  fourierdlem81  40907  fourierdlem89  40915  fourierdlem91  40917  fourierdlem92  40918  fourierdlem111  40937  fouriercn  40952  hspdifhsp  41336  srhmsubc  42586  srhmsubcALTV  42604  gsumsplit2f  42653  fdivmpt  42844  fdivpm  42847  refdivpm  42848  elpglem2  42968
  Copyright terms: Public domain W3C validator