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

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

Proof of Theorem sseqtrrid
StepHypRef Expression
1 sseqtrrid.1 . . 3 𝐵𝐴
21a1i 11 . 2 (𝜑𝐵𝐴)
3 sseqtrrid.2 . 2 (𝜑𝐶 = 𝐴)
42, 3sseqtrrd 4011 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  wss 3939
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2804  df-cleq 2818  df-clel 2897  df-in 3946  df-ss 3955
This theorem is referenced by:  unissint  4897  resdif  6631  fimacnv  6834  tfrlem5  8010  domss2  8668  dffi3  8887  cantnfp1lem3  9135  trcl  9162  tcid  9173  r1ordg  9199  r1sssuc  9204  ackbij1lem15  9648  cfsmolem  9684  fin1a2lem7  9820  wunex2  10152  wuncid  10157  trclfvlb  14361  rtrclreclem1  14410  fsumsplit  15090  o1fsum  15161  fprodsplit  15313  phimullem  16109  vdwlem6  16315  ressinbas  16553  mrcssid  16881  mreexexlem2d  16909  acsfiindd  17780  dirge  17840  symgbasfi  18437  efgredlemf  18790  efgredlemd  18793  gsumzres  18952  gsumzcl2  18953  gsumzf1o  18955  gsumadd  18966  gsumzsplit  18970  gsumsplit2  18972  dprd2da  19087  dmdprdsplit2lem  19090  dmdprdsplit2  19091  dmdprdsplit  19092  dprdsplit  19093  invrpropd  19371  issubdrg  19483  lspssid  19680  aspssid  20029  pjcss  20779  istopon  21439  sscls  21583  ordtbas  21719  cncls2  21800  tgcmp  21928  cmpfi  21935  1stcfb  21972  1stckgenlem  22080  ptbasfi  22108  ptcnplem  22148  ptuncnv  22334  ptunhmeo  22335  fbasrn  22411  cnflf2  22530  fclscmp  22557  alexsublem  22571  ghmcnp  22641  tsmsgsum  22665  tsmsres  22670  tsmssplit  22678  tsmsxplem1  22679  ustssco  22741  mopnfss  22971  cnmpopc  23450  uniiccdif  24097  uniioombllem3  24104  uniioombllem4  24105  itg2splitlem  24267  itg2split  24268  itgsplit  24354  ellimc2  24393  ellimc3  24395  lhop  24531  plyaddlem1  24721  plymullem1  24722  taylthlem2  24880  mtest  24910  xrlimcnp  25463  fsumharmonic  25506  chtdif  25652  dchrghm  25749  lgsquadlem2  25874  dchrisumlema  25981  dchrisumlem2  25983  dchrisum0lem1b  26008  dchrisum0lem1  26009  pntrlog2bndlem6  26076  pntlemf  26098  nbupgruvtxres  27106  umgr2adedgwlk  27641  umgr2adedgwlkon  27642  umgr2adedgspth  27644  ex-res  28137  spanss2  29039  mdsymi  30105  padct  30371  cycpmco2lem5  30689  cycpmco2lem6  30690  cycpmco2lem7  30691  cycpmco2  30692  ordtconnlem1  31056  issgon  31271  sssigagen  31293  measiuns  31365  sitgclg  31489  cvmliftlem10  32428  satfsschain  32498  fmlasssuc  32523  satfun  32545  rdgssun  34531  ftc1anclem6  34842  heibor1lem  34958  heibor  34970  divrngcl  35106  isdrngo2  35107  igenss  35211  paddunssN  36814  sspadd1  36821  sspadd2  36822  pclssidN  36901  diassdvaN  38066  dochvalr  38363  lcdvbase  38599  nacsfix  39177  isnumbasgrplem2  39572  rgspnssid  39638  itgpowd  39689  trrelsuperrel2dg  39884  fvilbd  39902  relexp0a  39929  wnefimgd  40380  grumnudlem  40489  icccncfext  42038  iblsplit  42119  dirkeritg  42256  dirkercncflem2  42258  fourierdlem81  42341  fourierdlem89  42349  fourierdlem91  42351  fourierdlem92  42352  fourierdlem111  42371  fouriercn  42386  hspdifhsp  42767  gsumsplit2f  43922  srhmsubc  44182  srhmsubcALTV  44200  fdivmpt  44435  fdivpm  44438  refdivpm  44439  elpglem2  44649
  Copyright terms: Public domain W3C validator