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

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

Proof of Theorem sseqtrid
StepHypRef Expression
1 sseqtrid.2 . 2 (𝜑𝐴 = 𝐶)
2 sseqtrid.1 . 2 𝐵𝐴
3 sseq2 3970 . . 3 (𝐴 = 𝐶 → (𝐵𝐴𝐵𝐶))
43biimpa 477 . 2 ((𝐴 = 𝐶𝐵𝐴) → 𝐵𝐶)
51, 2, 4sylancl 586 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1541  wss 3910
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3447  df-in 3917  df-ss 3927
This theorem is referenced by:  iunxdif3  5055  fssdm  6688  fndmdif  6992  fneqeql2  6997  fconst4  7163  isofrlem  7284  fvmptopab  7410  f1opw2  7607  fparlem3  8045  fparlem4  8046  fnwelem  8062  fsuppeq  8105  fsuppeqg  8106  ecss  8693  pw2f1olem  9019  fopwdom  9023  ssenen  9094  ssfiALT  9117  phplem2OLD  9161  fiint  9267  f1opwfi  9299  kmlem5  10089  enfin2i  10256  fpwwe2lem5  10570  fpwwe2lem8  10573  tskuni  10718  monoord2  13938  seqz  13955  cshimadifsn0  14718  binom1dif  15717  bpolycl  15934  bpolysum  15935  bpolydiflem  15936  bitsres  16352  prdshom  17348  imasless  17421  cntzval  19099  f1omvdmvd  19223  f1omvdconj  19226  pmtrfb  19245  symggen  19250  symggen2  19251  psgnunilem1  19273  gsumzaddlem  19696  isdrngd  20212  lspextmo  20515  znleval  20959  ordtcld1  22546  ordtcld2  22547  cnpnei  22613  cnntri  22620  cncls2  22622  cncls  22623  cnntr  22624  cncnp  22629  cndis  22640  paste  22643  cmpfi  22757  conncompcld  22783  1stcfb  22794  1stccnp  22811  cldllycmp  22844  llycmpkgen2  22899  kgencn  22905  kgencn3  22907  dfac14lem  22966  txdis1cn  22984  hausdiag  22994  txkgen  23001  qtopval2  23045  basqtop  23060  qtopcld  23062  qtopeu  23065  qtoprest  23066  imastopn  23069  hmeontr  23118  hmeoimaf1o  23119  cmphaushmeo  23149  ordthmeolem  23150  elfm3  23299  rnelfmlem  23301  rnelfm  23302  alexsubALTlem4  23399  cldsubg  23460  tgpconncompeqg  23461  tgpconncomp  23462  qustgpopn  23469  qustgplem  23470  tsmsf1o  23494  ucncn  23635  imasf1oxms  23843  blcld  23859  metustfbas  23911  cfilucfil  23913  metuel2  23919  icchmeo  24302  relcmpcmet  24680  minveclem4a  24792  nulmbl2  24898  icombl  24926  ioombl  24927  uniiccdif  24940  volivth  24969  mbfres2  25007  itg1addlem5  25063  itgsplitioo  25200  dvcobr  25308  dvcnvlem  25338  lhop1lem  25375  lhop  25378  dvcnvrelem2  25380  uc1pval  25502  mon1pval  25504  vieta1lem2  25669  basellem5  26432  f1otrg  27760  axlowdimlem13  27850  axcontlem10  27869  uhgrspansubgr  28186  vtxdun  28376  pthdlem1  28661  eucrct2eupth  29136  ssmd1  31200  mdslj2i  31209  atcvat4i  31286  imadifxp  31466  nfpconfp  31493  2ndresdju  31512  ofpreima  31528  ofpreima2  31529  fsuppcurry1  31586  fsuppcurry2  31587  gsumpart  31841  symgcom  31878  symgcom2  31879  pmtrcnel  31884  cycpmfvlem  31905  cycpmfv3  31908  freshmansdream  32011  elrspunidl  32143  idlinsubrg  32145  qtophaus  32357  reff  32360  locfinreflem  32361  zarcmplem  32402  hauseqcn  32419  indpreima  32564  indf1ofs  32565  oms0  32837  eulerpartlemv  32904  eulerpartlemb  32908  eulerpartlemr  32914  eulerpartlemgs2  32920  eulerpartlemn  32921  ballotlemro  33062  bnj1253  33569  bnj1280  33572  pthhashvtx  33661  acycgr0v  33682  prclisacycgr  33685  subfacp1lem3  33716  cvmscld  33807  cvmsss2  33808  cvmliftmolem1  33815  cvmliftlem7  33825  cvmlift2lem9  33845  cvmlift3lem7  33859  fnessref  34819  tailf  34837  poimirlem3  36071  mbfresfi  36114  cnambfre  36116  itg2addnclem2  36120  mettrifi  36206  ismtyres  36257  isdrngo2  36407  diaintclN  39511  dibintclN  39620  dihintcl  39797  dochocss  39819  mapdunirnN  40103  pw2f1ocnv  41338  wessf1ornlem  43378  monoord2xrv  43694  itgcoscmulx  44181  ibliooicc  44183  stoweidlem11  44223  stoweidlem34  44246  fourierdlem48  44366  fourierdlem49  44367  fourierdlem74  44392  uniimaprimaeqfv  45545  elsetpreimafvssdm  45549  rngcbas  46234  ringcbas  46280  fdivmptf  46598  refdivmptf  46599  iscnrm3llem2  46954
  Copyright terms: Public domain W3C validator