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

Theorem sseqtrid 4022
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 3996 . . 3 (𝐴 = 𝐶 → (𝐵𝐴𝐵𝐶))
43biimpa 477 . 2 ((𝐴 = 𝐶𝐵𝐴) → 𝐵𝐶)
51, 2, 4sylancl 586 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:  iunxdif3  5013  fssdm  6526  fndmdif  6807  fneqeql2  6812  fconst4  6975  isofrlem  7088  f1opw2  7393  fparlem3  7803  fparlem4  7804  fnwelem  7819  frnsuppeq  7836  ecss  8328  pw2f1olem  8613  fopwdom  8617  ssenen  8683  phplem2  8689  ssfi  8730  fiint  8787  f1opwfi  8820  kmlem5  9572  enfin2i  9735  fpwwe2lem6  10049  fpwwe2lem9  10052  tskuni  10197  monoord2  13394  seqz  13411  cshimadifsn0  14185  binom1dif  15180  bpolycl  15398  bpolysum  15399  bpolydiflem  15400  bitsres  15814  prdshom  16732  imasless  16805  cntzval  18383  f1omvdmvd  18493  f1omvdconj  18496  pmtrfb  18515  symggen  18520  symggen2  18521  psgnunilem1  18543  gsumzaddlem  18963  isdrngd  19449  lspextmo  19750  znleval  20619  ordtcld1  21723  ordtcld2  21724  cnpnei  21790  cnntri  21797  cncls2  21799  cncls  21800  cnntr  21801  cncnp  21806  cndis  21817  paste  21820  cmpfi  21934  conncompcld  21960  1stcfb  21971  1stccnp  21988  cldllycmp  22021  llycmpkgen2  22076  kgencn  22082  kgencn3  22084  dfac14lem  22143  txdis1cn  22161  hausdiag  22171  txkgen  22178  qtopval2  22222  basqtop  22237  qtopcld  22239  qtopeu  22242  qtoprest  22243  imastopn  22246  hmeontr  22295  hmeoimaf1o  22296  cmphaushmeo  22326  ordthmeolem  22327  elfm3  22476  rnelfmlem  22478  rnelfm  22479  alexsubALTlem4  22576  cldsubg  22636  tgpconncompeqg  22637  tgpconncomp  22638  qustgpopn  22645  qustgplem  22646  tsmsf1o  22670  ucncn  22811  imasf1oxms  23016  blcld  23032  metustfbas  23084  cfilucfil  23086  metuel2  23092  icchmeo  23462  relcmpcmet  23838  minveclem4a  23950  nulmbl2  24054  icombl  24082  ioombl  24083  uniiccdif  24096  volivth  24125  mbfres2  24163  itg1addlem5  24218  itgsplitioo  24355  dvcobr  24460  dvcnvlem  24490  lhop1lem  24527  lhop  24530  dvcnvrelem2  24532  uc1pval  24650  mon1pval  24652  vieta1lem2  24817  basellem5  25578  f1otrg  26573  axlowdimlem13  26656  axcontlem10  26675  uhgrspansubgr  26989  vtxdun  27179  pthdlem1  27463  eucrct2eupth  27940  ssmd1  30004  mdslj2i  30013  atcvat4i  30090  imadifxp  30268  nfpconfp  30294  ofpreima  30327  ofpreima2  30328  fsuppcurry1  30376  fsuppcurry2  30377  symgcom  30643  symgcom2  30644  pmtrcnel  30649  cycpmfvlem  30670  cycpmfv3  30673  freshmansdream  30775  qtophaus  30988  reff  30991  locfinreflem  30992  hauseqcn  31026  indpreima  31172  indf1ofs  31173  oms0  31443  eulerpartlemv  31510  eulerpartlemb  31514  eulerpartlemr  31520  eulerpartlemgs2  31526  eulerpartlemn  31527  ballotlemro  31668  bnj1253  32175  bnj1280  32178  pthhashvtx  32260  acycgr0v  32281  prclisacycgr  32284  subfacp1lem3  32315  cvmscld  32406  cvmsss2  32407  cvmliftmolem1  32414  cvmliftlem7  32424  cvmlift2lem9  32444  cvmlift3lem7  32458  fnessref  33591  tailf  33609  poimirlem3  34764  mbfresfi  34807  cnambfre  34809  itg2addnclem2  34813  mettrifi  34902  ismtyres  34956  isdrngo2  35106  diaintclN  38063  dibintclN  38172  dihintcl  38349  dochocss  38371  mapdunirnN  38655  pw2f1ocnv  39501  wessf1ornlem  41312  monoord2xrv  41627  itgcoscmulx  42121  ibliooicc  42123  stoweidlem11  42164  stoweidlem34  42187  fourierdlem48  42307  fourierdlem49  42308  fourierdlem74  42333  rngcbas  44070  ringcbas  44116  fdivmptf  44435  refdivmptf  44436
  Copyright terms: Public domain W3C validator