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

Step	Hyp	Ref	Expression
1		sseqtrid.1	. . 3 ⊢ 𝐵 ⊆ 𝐴
2	1	a1i 11	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐴)
3		sseqtrid.2	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	2, 3	sseqtrd 3968	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3899

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3916

This theorem is referenced by:  sseqtrrid  3975  iunxdif3  5047  fssdm  6678  fndmdif  6984  fneqeql2  6989  fconst4  7157  isofrlem  7283  fvmptopab  7410  f1opw2  7610  fparlem3  8053  fparlem4  8054  fnwelem  8070  fsuppeq  8114  fsuppeqg  8115  ecss  8682  pw2f1olem  9004  fopwdom  9008  ssenen  9074  ssfiALT  9093  fiint  9221  f1opwfi  9250  kmlem5  10056  enfin2i  10222  fpwwe2lem5  10536  fpwwe2lem8  10539  tskuni  10684  monoord2  13950  seqz  13967  cshimadifsn0  14747  binom1dif  15750  bpolycl  15969  bpolysum  15970  bpolydiflem  15971  bitsres  16394  prdshom  17381  imasless  17454  cntzval  19243  f1omvdmvd  19365  f1omvdconj  19368  pmtrfb  19387  symggen  19392  symggen2  19393  psgnunilem1  19415  gsumzaddlem  19843  rngcbas  20546  ringcbas  20575  isdrngd  20690  isdrngdOLD  20692  lspextmo  21000  znleval  21501  freshmansdream  21521  ordtcld1  23122  ordtcld2  23123  cnpnei  23189  cnntri  23196  cncls2  23198  cncls  23199  cnntr  23200  cncnp  23205  cndis  23216  paste  23219  cmpfi  23333  conncompcld  23359  1stcfb  23370  1stccnp  23387  cldllycmp  23420  llycmpkgen2  23475  kgencn  23481  kgencn3  23483  dfac14lem  23542  txdis1cn  23560  hausdiag  23570  txkgen  23577  qtopval2  23621  basqtop  23636  qtopcld  23638  qtopeu  23641  qtoprest  23642  imastopn  23645  hmeontr  23694  hmeoimaf1o  23695  cmphaushmeo  23725  ordthmeolem  23726  elfm3  23875  rnelfmlem  23877  rnelfm  23878  alexsubALTlem4  23975  cldsubg  24036  tgpconncompeqg  24037  tgpconncomp  24038  qustgpopn  24045  qustgplem  24046  tsmsf1o  24070  ucncn  24209  imasf1oxms  24414  blcld  24430  metustfbas  24482  cfilucfil  24484  metuel2  24490  icchmeo  24875  icchmeoOLD  24876  relcmpcmet  25255  minveclem4a  25367  nulmbl2  25474  icombl  25502  ioombl  25503  uniiccdif  25516  volivth  25545  mbfres2  25583  itg1addlem5  25638  itgsplitioo  25776  dvcobr  25886  dvcobrOLD  25887  dvcnvlem  25917  lhop1lem  25955  lhop  25958  dvcnvrelem2  25960  uc1pval  26082  mon1pval  26084  vieta1lem2  26256  basellem5  27032  onnolt  28213  f1otrg  28859  axlowdimlem13  28943  axcontlem10  28962  uhgrspansubgr  29280  vtxdun  29471  pthdlem1  29755  eucrct2eupth  30236  ssmd1  32302  mdslj2i  32311  atcvat4i  32388  imadifxp  32592  nfpconfp  32625  2ndresdju  32642  ofpreima  32658  ofpreima2  32659  fsuppcurry1  32718  fsuppcurry2  32719  indpreima  32857  indf1ofs  32858  ccatws1f1olast  32944  gsumpart  33048  symgcom  33063  symgcom2  33064  pmtrcnel  33069  cycpmfvlem  33092  cycpmfv3  33095  elrgspnsubrunlem2  33226  elrspunidl  33404  idlinsubrg  33407  esplymhp  33600  fldextrspunlsp  33698  qtophaus  33860  reff  33863  locfinreflem  33864  zarcmplem  33905  hauseqcn  33922  oms0  34321  eulerpartlemv  34388  eulerpartlemb  34392  eulerpartlemr  34398  eulerpartlemgs2  34404  eulerpartlemn  34405  ballotlemro  34547  bnj1253  35040  bnj1280  35043  pthhashvtx  35183  acycgr0v  35203  prclisacycgr  35206  subfacp1lem3  35237  cvmscld  35328  cvmsss2  35329  cvmliftmolem1  35336  cvmliftlem7  35346  cvmlift2lem9  35366  cvmlift3lem7  35380  fnessref  36412  tailf  36430  poimirlem3  37673  mbfresfi  37716  cnambfre  37718  itg2addnclem2  37722  mettrifi  37807  ismtyres  37858  isdrngo2  38008  press  38521  diaintclN  41167  dibintclN  41276  dihintcl  41453  dochocss  41475  mapdunirnN  41759  pw2f1ocnv  43144  wessf1ornlem  45296  monoord2xrv  45595  itgcoscmulx  46081  ibliooicc  46083  stoweidlem11  46123  stoweidlem34  46146  fourierdlem48  46266  fourierdlem49  46267  fourierdlem74  46292  uniimaprimaeqfv  47496  elsetpreimafvssdm  47500  fdivmptf  48656  refdivmptf  48657  iscnrm3llem2  49064  imaidfu  49225