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

Theorem syl5sseqr 3687
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 3675 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  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:  unissint  4533  resdif  6195  fimacnv  6387  tfrlem5  7521  domss2  8160  dffi3  8378  cantnfp1lem3  8615  trcl  8642  tcid  8653  r1ordg  8679  r1sssuc  8684  ackbij1lem15  9094  cfsmolem  9130  isfin4-3  9175  fin1a2lem7  9266  wunex2  9598  wuncid  9603  trclfvlb  13793  rtrclreclem1  13842  fsumsplit  14515  o1fsum  14589  fprodsplit  14740  phimullem  15531  vdwlem6  15737  ressinbas  15983  mrcssid  16324  mreexexlem2d  16352  acsfiindd  17224  dirge  17284  symgbasfi  17852  efgredlemf  18200  efgredlemd  18203  gsumzres  18356  gsumzcl2  18357  gsumzf1o  18359  gsumadd  18369  gsumzsplit  18373  gsumsplit2  18375  dprd2da  18487  dmdprdsplit2lem  18490  dmdprdsplit2  18491  dmdprdsplit  18492  dprdsplit  18493  invrpropd  18744  issubdrg  18853  lspssid  19033  aspssid  19381  pjcss  20108  istopon  20765  sscls  20908  ordtbas  21044  cncls2  21125  tgcmp  21252  cmpfi  21259  1stcfb  21296  1stckgenlem  21404  ptbasfi  21432  ptcnplem  21472  ptuncnv  21658  ptunhmeo  21659  fbasrn  21735  cnflf2  21854  fclscmp  21881  alexsublem  21895  ghmcnp  21965  tsmsgsum  21989  tsmsres  21994  tsmssplit  22002  tsmsxplem1  22003  ustssco  22065  mopnfss  22295  cnmpt2pc  22774  uniiccdif  23392  uniioombllem3  23399  uniioombllem4  23400  itg2splitlem  23560  itg2split  23561  itgsplit  23647  ellimc2  23686  ellimc3  23688  lhop  23824  plyaddlem1  24014  plymullem1  24015  taylthlem2  24173  mtest  24203  xrlimcnp  24740  fsumharmonic  24783  chtdif  24929  dchrghm  25026  lgsquadlem2  25151  dchrisumlema  25222  dchrisumlem2  25224  dchrisum0lem1b  25249  dchrisum0lem1  25250  pntrlog2bndlem6  25317  pntlemf  25339  nbupgruvtxres  26358  umgr2adedgwlk  26910  umgr2adedgwlkon  26911  umgr2adedgspth  26913  ex-res  27428  spanss2  28332  mdsymi  29398  padct  29625  ordtconnlem1  30098  issgon  30314  sssigagen  30336  measiuns  30408  sitgclg  30532  cvmliftlem10  31402  ftc1anclem6  33620  heibor1lem  33738  heibor  33750  divrngcl  33886  isdrngo2  33887  igenss  33991  paddunssN  35412  sspadd1  35419  sspadd2  35420  pclssidN  35499  diassdvaN  36666  dochvalr  36963  lcdvbase  37199  nacsfix  37592  isnumbasgrplem2  37991  rgspnssid  38057  itgpowd  38117  trrelsuperrel2dg  38280  fvilbd  38298  relexp0a  38325  wnefimgd  38777  icccncfext  40418  iblsplit  40500  dirkeritg  40637  dirkercncflem2  40639  fourierdlem81  40722  fourierdlem89  40730  fourierdlem91  40732  fourierdlem92  40733  fourierdlem111  40752  fouriercn  40767  hspdifhsp  41151  srhmsubc  42401  srhmsubcALTV  42419  gsumsplit2f  42468  fdivmpt  42659  fdivpm  42662  refdivpm  42663  elpglem2  42783
  Copyright terms: Public domain W3C validator