Theorem sseqtrid 3973

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 3967	1 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2753  df-ss 3916

This theorem is used by:  sseqtrrid  3974  iunxdif3  5055  fssdm  6721  fndmdif  7033  fneqeql2  7038  fconst4  7212  isofrlem  7340  fvmptopab  7467  f1opw2  7668  fparlem3  8114  fparlem4  8115  fnwelem  8132  fsuppeq  8176  fsuppeqg  8177  ecss  8753  pw2f1olem  9084  fopwdom  9088  ssenen  9154  ssfiALT  9173  fiint  9302  f1opwfi  9329  kmlem5  10214  enfin2i  10380  fpwwe2lem5  10701  fpwwe2lem8  10704  tskuni  10849  monoord2  14156  seqz  14173  cshimadifsn0  14961  binom1dif  15982  bpolycl  16198  bpolysum  16199  bpolydiflem  16200  bitsres  16623  prdshom  17618  imasless  17692  cntzval  19515  f1omvdmvd  19637  f1omvdconj  19640  pmtrfb  19659  symggen  19664  symggen2  19665  psgnunilem1  19687  gsumzaddlem  20115  rngcbas  20853  ringcbas  20882  isdrngd  21002  isdrngdOLD  21004  lspextmo  21311  znleval  21840  freshmansdream  21860  ordtcld1  23495  ordtcld2  23496  cnpnei  23562  cnntri  23569  cncls2  23571  cncls  23572  cnntr  23573  cncnp  23578  cndis  23589  paste  23592  cmpfi  23706  conncompcld  23732  1stcfb  23743  1stccnp  23761  cldllycmp  23794  llycmpkgen2  23849  kgencn  23855  kgencn3  23857  dfac14lem  23916  txdis1cn  23934  hausdiag  23944  txkgen  23951  qtopval2  23995  basqtop  24010  qtopcld  24012  qtopeu  24015  qtoprest  24016  imastopn  24019  hmeontr  24068  hmeoimaf1o  24069  cmphaushmeo  24099  ordthmeolem  24100  elfm3  24249  rnelfmlem  24251  rnelfm  24252  alexsubALTlem4  24349  cldsubg  24410  tgpconncompeqg  24411  tgpconncomp  24412  qustgpopn  24419  qustgplem  24420  tsmsf1o  24444  ucncn  24583  imasf1oxms  24788  blcld  24804  metustfbas  24856  cfilucfil  24858  metuel2  24864  icchmeo  25242  relcmpcmet  25619  minveclem4a  25731  nulmbl2  25837  icombl  25865  ioombl  25866  uniiccdif  25879  volivth  25908  mbfres2  25946  itg1addlem5  26001  itgsplitioo  26138  dvcobr  26246  dvcnvlem  26276  lhop1lem  26313  lhop  26316  dvcnvrelem2  26318  uc1pval  26438  mon1pval  26440  vieta1lem2  26616  basellem5  27394  onnolt  28634  f1otrg  29430  axlowdimlem13  29514  axcontlem10  29533  uhgrspansubgr  29854  vtxdun  30044  pthhashvtx  30297  pthdlem1  30334  eucrct2eupth  30828  ssmd1  32895  mdslj2i  32904  atcvat4i  32981  imadifxp  33177  nfpconfp  33208  2ndresdju  33225  ofpreima  33241  ofpreima2  33242  fsuppcurry1  33298  fsuppcurry2  33299  indpreima  33414  indf1ofs  33415  ccatws1f1olast  33497  gsumpart  33606  symgcom  33626  symgcom2  33627  pmtrcnel  33632  cycpmfvlem  33655  cycpmfv3  33658  elrgspnsubrunlem2  33791  elrspunidl  33960  idlinsubrg  33963  esplymhp  34182  esplyfval1  34187  esplyfvaln  34188  fldextrspunlsp  34288  qtophaus  34450  reff  34453  locfinreflem  34454  zarcmplem  34495  hauseqcn  34512  oms0  34912  eulerpartlemv  34979  eulerpartlemb  34983  eulerpartlemr  34989  eulerpartlemgs2  34995  eulerpartlemn  34996  ballotlemro  35138  bnj1253  35630  bnj1280  35633  onvfowev  35868  acycgr0v  35882  prclisacycgr  35885  subfacp1lem3  35916  cvmscld  36007  cvmsss2  36008  cvmliftmolem1  36015  cvmliftlem7  36025  cvmlift2lem9  36045  cvmlift3lem7  36059  fnessref  37115  tailf  37133  poimirlem3  38509  mbfresfi  38552  cnambfre  38554  itg2addnclem2  38558  mettrifi  38659  ismtyres  38710  isdrngo2  38860  press  39399  diaintclN  42083  dibintclN  42192  dihintcl  42369  dochocss  42391  mapdunirnN  42675  pw2f1ocnv  43997  wessf1ornlem  46143  monoord2xrv  46437  itgcoscmulx  46923  ibliooicc  46925  stoweidlem11  46965  stoweidlem34  46988  fourierdlem48  47108  fourierdlem49  47109  fourierdlem74  47134  tmachlem-agreeprod  47891  uniimaprimaeqfv  48408  elsetpreimafvssdm  48412  fdivmptf  49597  refdivmptf  49598  iscnrm3llem2  50002  imaidfu  50162