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

Theorem sseqtrid 3974
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 3948 . . 3 (𝐴 = 𝐶 → (𝐵𝐴𝐵𝐶))
43biimpa 477 . 2 ((𝐴 = 𝐶𝐵𝐴) → 𝐵𝐶)
51, 2, 4sylancl 586 1 (𝜑𝐵𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1539  wss 3888
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710
This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905
This theorem is referenced by:  iunxdif3  5025  fssdm  6629  fndmdif  6928  fneqeql2  6933  fconst4  7099  isofrlem  7220  fvmptopab  7338  f1opw2  7533  fparlem3  7963  fparlem4  7964  fnwelem  7981  frnsuppeq  8000  frnsuppeqg  8001  ecss  8553  pw2f1olem  8872  fopwdom  8876  ssenen  8947  ssfiALT  8966  phplem2OLD  9010  fiint  9100  f1opwfi  9132  kmlem5  9919  enfin2i  10086  fpwwe2lem5  10400  fpwwe2lem8  10403  tskuni  10548  monoord2  13763  seqz  13780  cshimadifsn0  14552  binom1dif  15554  bpolycl  15771  bpolysum  15772  bpolydiflem  15773  bitsres  16189  prdshom  17187  imasless  17260  cntzval  18936  f1omvdmvd  19060  f1omvdconj  19063  pmtrfb  19082  symggen  19087  symggen2  19088  psgnunilem1  19110  gsumzaddlem  19531  isdrngd  20025  lspextmo  20327  znleval  20771  ordtcld1  22357  ordtcld2  22358  cnpnei  22424  cnntri  22431  cncls2  22433  cncls  22434  cnntr  22435  cncnp  22440  cndis  22451  paste  22454  cmpfi  22568  conncompcld  22594  1stcfb  22605  1stccnp  22622  cldllycmp  22655  llycmpkgen2  22710  kgencn  22716  kgencn3  22718  dfac14lem  22777  txdis1cn  22795  hausdiag  22805  txkgen  22812  qtopval2  22856  basqtop  22871  qtopcld  22873  qtopeu  22876  qtoprest  22877  imastopn  22880  hmeontr  22929  hmeoimaf1o  22930  cmphaushmeo  22960  ordthmeolem  22961  elfm3  23110  rnelfmlem  23112  rnelfm  23113  alexsubALTlem4  23210  cldsubg  23271  tgpconncompeqg  23272  tgpconncomp  23273  qustgpopn  23280  qustgplem  23281  tsmsf1o  23305  ucncn  23446  imasf1oxms  23654  blcld  23670  metustfbas  23722  cfilucfil  23724  metuel2  23730  icchmeo  24113  relcmpcmet  24491  minveclem4a  24603  nulmbl2  24709  icombl  24737  ioombl  24738  uniiccdif  24751  volivth  24780  mbfres2  24818  itg1addlem5  24874  itgsplitioo  25011  dvcobr  25119  dvcnvlem  25149  lhop1lem  25186  lhop  25189  dvcnvrelem2  25191  uc1pval  25313  mon1pval  25315  vieta1lem2  25480  basellem5  26243  f1otrg  27241  axlowdimlem13  27331  axcontlem10  27350  uhgrspansubgr  27667  vtxdun  27857  pthdlem1  28143  eucrct2eupth  28618  ssmd1  30682  mdslj2i  30691  atcvat4i  30768  imadifxp  30949  nfpconfp  30976  2ndresdju  30995  ofpreima  31011  ofpreima2  31012  fsuppcurry1  31069  fsuppcurry2  31070  gsumpart  31324  symgcom  31361  symgcom2  31362  pmtrcnel  31367  cycpmfvlem  31388  cycpmfv3  31391  freshmansdream  31493  elrspunidl  31615  idlinsubrg  31617  qtophaus  31795  reff  31798  locfinreflem  31799  zarcmplem  31840  hauseqcn  31857  indpreima  32002  indf1ofs  32003  oms0  32273  eulerpartlemv  32340  eulerpartlemb  32344  eulerpartlemr  32350  eulerpartlemgs2  32356  eulerpartlemn  32357  ballotlemro  32498  bnj1253  33006  bnj1280  33009  pthhashvtx  33098  acycgr0v  33119  prclisacycgr  33122  subfacp1lem3  33153  cvmscld  33244  cvmsss2  33245  cvmliftmolem1  33252  cvmliftlem7  33262  cvmlift2lem9  33282  cvmlift3lem7  33296  fnessref  34555  tailf  34573  poimirlem3  35789  mbfresfi  35832  cnambfre  35834  itg2addnclem2  35838  mettrifi  35924  ismtyres  35975  isdrngo2  36125  diaintclN  39079  dibintclN  39188  dihintcl  39365  dochocss  39387  mapdunirnN  39671  pw2f1ocnv  40866  wessf1ornlem  42729  monoord2xrv  43031  itgcoscmulx  43517  ibliooicc  43519  stoweidlem11  43559  stoweidlem34  43582  fourierdlem48  43702  fourierdlem49  43703  fourierdlem74  43728  uniimaprimaeqfv  44845  elsetpreimafvssdm  44849  rngcbas  45534  ringcbas  45580  fdivmptf  45898  refdivmptf  45899  iscnrm3llem2  46255
  Copyright terms: Public domain W3C validator