Theorem sseqtrid 3965

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  sseqtrrid  3966  iunxdif3  5038  fssdm  6681  fndmdif  6988  fneqeql2  6993  fconst4  7162  isofrlem  7288  fvmptopab  7415  f1opw2  7615  fparlem3  8057  fparlem4  8058  fnwelem  8074  fsuppeq  8118  fsuppeqg  8119  ecss  8688  pw2f1olem  9012  fopwdom  9016  ssenen  9082  ssfiALT  9101  fiint  9230  f1opwfi  9259  kmlem5  10068  enfin2i  10234  fpwwe2lem5  10549  fpwwe2lem8  10552  tskuni  10697  monoord2  13986  seqz  14003  cshimadifsn0  14783  binom1dif  15789  bpolycl  16008  bpolysum  16009  bpolydiflem  16010  bitsres  16433  prdshom  17421  imasless  17495  cntzval  19287  f1omvdmvd  19409  f1omvdconj  19412  pmtrfb  19431  symggen  19436  symggen2  19437  psgnunilem1  19459  gsumzaddlem  19887  rngcbas  20589  ringcbas  20618  isdrngd  20733  isdrngdOLD  20735  lspextmo  21043  znleval  21544  freshmansdream  21564  ordtcld1  23172  ordtcld2  23173  cnpnei  23239  cnntri  23246  cncls2  23248  cncls  23249  cnntr  23250  cncnp  23255  cndis  23266  paste  23269  cmpfi  23383  conncompcld  23409  1stcfb  23420  1stccnp  23437  cldllycmp  23470  llycmpkgen2  23525  kgencn  23531  kgencn3  23533  dfac14lem  23592  txdis1cn  23610  hausdiag  23620  txkgen  23627  qtopval2  23671  basqtop  23686  qtopcld  23688  qtopeu  23691  qtoprest  23692  imastopn  23695  hmeontr  23744  hmeoimaf1o  23745  cmphaushmeo  23775  ordthmeolem  23776  elfm3  23925  rnelfmlem  23927  rnelfm  23928  alexsubALTlem4  24025  cldsubg  24086  tgpconncompeqg  24087  tgpconncomp  24088  qustgpopn  24095  qustgplem  24096  tsmsf1o  24120  ucncn  24259  imasf1oxms  24464  blcld  24480  metustfbas  24532  cfilucfil  24534  metuel2  24540  icchmeo  24918  relcmpcmet  25295  minveclem4a  25407  nulmbl2  25513  icombl  25541  ioombl  25542  uniiccdif  25555  volivth  25584  mbfres2  25622  itg1addlem5  25677  itgsplitioo  25815  dvcobr  25923  dvcnvlem  25953  lhop1lem  25990  lhop  25993  dvcnvrelem2  25995  uc1pval  26115  mon1pval  26117  vieta1lem2  26288  basellem5  27062  onnolt  28272  f1otrg  28953  axlowdimlem13  29037  axcontlem10  29056  uhgrspansubgr  29374  vtxdun  29565  pthdlem1  29849  eucrct2eupth  30330  ssmd1  32397  mdslj2i  32406  atcvat4i  32483  imadifxp  32686  nfpconfp  32720  2ndresdju  32737  ofpreima  32753  ofpreima2  32754  fsuppcurry1  32812  fsuppcurry2  32813  indpreima  32940  indf1ofs  32941  ccatws1f1olast  33027  gsumpart  33139  symgcom  33159  symgcom2  33160  pmtrcnel  33165  cycpmfvlem  33188  cycpmfv3  33191  elrgspnsubrunlem2  33324  elrspunidl  33503  idlinsubrg  33506  esplymhp  33727  esplyfval1  33732  esplyfvaln  33733  fldextrspunlsp  33834  qtophaus  33996  reff  33999  locfinreflem  34000  zarcmplem  34041  hauseqcn  34058  oms0  34457  eulerpartlemv  34524  eulerpartlemb  34528  eulerpartlemr  34534  eulerpartlemgs2  34540  eulerpartlemn  34541  ballotlemro  34683  bnj1253  35175  bnj1280  35178  pthhashvtx  35326  acycgr0v  35346  prclisacycgr  35349  subfacp1lem3  35380  cvmscld  35471  cvmsss2  35472  cvmliftmolem1  35479  cvmliftlem7  35489  cvmlift2lem9  35509  cvmlift3lem7  35523  fnessref  36555  tailf  36573  poimirlem3  37958  mbfresfi  38001  cnambfre  38003  itg2addnclem2  38007  mettrifi  38092  ismtyres  38143  isdrngo2  38293  press  38834  diaintclN  41518  dibintclN  41627  dihintcl  41804  dochocss  41826  mapdunirnN  42110  pw2f1ocnv  43483  wessf1ornlem  45633  monoord2xrv  45929  itgcoscmulx  46415  ibliooicc  46417  stoweidlem11  46457  stoweidlem34  46480  fourierdlem48  46600  fourierdlem49  46601  fourierdlem74  46626  uniimaprimaeqfv  47854  elsetpreimafvssdm  47858  fdivmptf  49029  refdivmptf  49030  iscnrm3llem2  49437  imaidfu  49597