Theorem sseqtrid 4048

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3963

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1777  df-cleq 2727  df-ss 3980

This theorem is referenced by:  sseqtrrid  4049  iunxdif3  5100  fssdm  6756  fndmdif  7062  fneqeql2  7067  fconst4  7234  isofrlem  7360  fvmptopab  7487  f1opw2  7688  fparlem3  8138  fparlem4  8139  fnwelem  8155  fsuppeq  8199  fsuppeqg  8200  ecss  8792  pw2f1olem  9115  fopwdom  9119  ssenen  9190  ssfiALT  9213  phplem2OLD  9253  fiint  9364  fiintOLD  9365  f1opwfi  9394  kmlem5  10193  enfin2i  10359  fpwwe2lem5  10673  fpwwe2lem8  10676  tskuni  10821  monoord2  14071  seqz  14088  cshimadifsn0  14866  binom1dif  15866  bpolycl  16085  bpolysum  16086  bpolydiflem  16087  bitsres  16507  prdshom  17514  imasless  17587  cntzval  19352  f1omvdmvd  19476  f1omvdconj  19479  pmtrfb  19498  symggen  19503  symggen2  19504  psgnunilem1  19526  gsumzaddlem  19954  rngcbas  20638  ringcbas  20667  isdrngd  20782  isdrngdOLD  20784  lspextmo  21073  znleval  21591  freshmansdream  21611  ordtcld1  23221  ordtcld2  23222  cnpnei  23288  cnntri  23295  cncls2  23297  cncls  23298  cnntr  23299  cncnp  23304  cndis  23315  paste  23318  cmpfi  23432  conncompcld  23458  1stcfb  23469  1stccnp  23486  cldllycmp  23519  llycmpkgen2  23574  kgencn  23580  kgencn3  23582  dfac14lem  23641  txdis1cn  23659  hausdiag  23669  txkgen  23676  qtopval2  23720  basqtop  23735  qtopcld  23737  qtopeu  23740  qtoprest  23741  imastopn  23744  hmeontr  23793  hmeoimaf1o  23794  cmphaushmeo  23824  ordthmeolem  23825  elfm3  23974  rnelfmlem  23976  rnelfm  23977  alexsubALTlem4  24074  cldsubg  24135  tgpconncompeqg  24136  tgpconncomp  24137  qustgpopn  24144  qustgplem  24145  tsmsf1o  24169  ucncn  24310  imasf1oxms  24518  blcld  24534  metustfbas  24586  cfilucfil  24588  metuel2  24594  icchmeo  24985  icchmeoOLD  24986  relcmpcmet  25366  minveclem4a  25478  nulmbl2  25585  icombl  25613  ioombl  25614  uniiccdif  25627  volivth  25656  mbfres2  25694  itg1addlem5  25750  itgsplitioo  25888  dvcobr  25998  dvcobrOLD  25999  dvcnvlem  26029  lhop1lem  26067  lhop  26070  dvcnvrelem2  26072  uc1pval  26194  mon1pval  26196  vieta1lem2  26368  basellem5  27143  f1otrg  28894  axlowdimlem13  28984  axcontlem10  29003  uhgrspansubgr  29323  vtxdun  29514  pthdlem1  29799  eucrct2eupth  30274  ssmd1  32340  mdslj2i  32349  atcvat4i  32426  imadifxp  32621  nfpconfp  32649  2ndresdju  32666  ofpreima  32682  ofpreima2  32683  fsuppcurry1  32743  fsuppcurry2  32744  ccatws1f1olast  32922  gsumpart  33043  symgcom  33086  symgcom2  33087  pmtrcnel  33092  cycpmfvlem  33115  cycpmfv3  33118  elrspunidl  33436  idlinsubrg  33439  qtophaus  33797  reff  33800  locfinreflem  33801  zarcmplem  33842  hauseqcn  33859  indpreima  34006  indf1ofs  34007  oms0  34279  eulerpartlemv  34346  eulerpartlemb  34350  eulerpartlemr  34356  eulerpartlemgs2  34362  eulerpartlemn  34363  ballotlemro  34504  bnj1253  35010  bnj1280  35013  pthhashvtx  35112  acycgr0v  35133  prclisacycgr  35136  subfacp1lem3  35167  cvmscld  35258  cvmsss2  35259  cvmliftmolem1  35266  cvmliftlem7  35276  cvmlift2lem9  35296  cvmlift3lem7  35310  fnessref  36340  tailf  36358  poimirlem3  37610  mbfresfi  37653  cnambfre  37655  itg2addnclem2  37659  mettrifi  37744  ismtyres  37795  isdrngo2  37945  diaintclN  41041  dibintclN  41150  dihintcl  41327  dochocss  41349  mapdunirnN  41633  pw2f1ocnv  43026  wessf1ornlem  45128  monoord2xrv  45434  itgcoscmulx  45925  ibliooicc  45927  stoweidlem11  45967  stoweidlem34  45990  fourierdlem48  46110  fourierdlem49  46111  fourierdlem74  46136  uniimaprimaeqfv  47307  elsetpreimafvssdm  47311  fdivmptf  48391  refdivmptf  48392  iscnrm3llem2  48747