Theorem sseqtrid 3981

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

Syntax hints:   → wi 4   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  sseqtrrid  3982  iunxdif3  5057  fssdm  6715  fndmdif  7027  fneqeql2  7032  fconst4  7202  isofrlem  7328  fvmptopab  7455  f1opw2  7655  fparlem3  8097  fparlem4  8098  fnwelem  8115  fsuppeq  8159  fsuppeqg  8160  ecss  8734  pw2f1olem  9057  fopwdom  9061  ssenen  9127  ssfiALT  9146  fiint  9274  f1opwfi  9301  kmlem5  10126  enfin2i  10293  fpwwe2lem5  10608  fpwwe2lem8  10611  tskuni  10756  monoord2  14060  seqz  14077  cshimadifsn0  14857  binom1dif  15877  bpolycl  16096  bpolysum  16097  bpolydiflem  16098  bitsres  16521  prdshom  17510  imasless  17584  cntzval  19382  f1omvdmvd  19504  f1omvdconj  19507  pmtrfb  19526  symggen  19531  symggen2  19532  psgnunilem1  19554  gsumzaddlem  19982  rngcbas  20697  ringcbas  20726  isdrngd  20838  isdrngdOLD  20840  lspextmo  21146  znleval  21664  freshmansdream  21684  ordtcld1  23315  ordtcld2  23316  cnpnei  23382  cnntri  23389  cncls2  23391  cncls  23392  cnntr  23393  cncnp  23398  cndis  23409  paste  23412  cmpfi  23526  conncompcld  23552  1stcfb  23563  1stccnp  23580  cldllycmp  23613  llycmpkgen2  23668  kgencn  23674  kgencn3  23676  dfac14lem  23735  txdis1cn  23753  hausdiag  23763  txkgen  23770  qtopval2  23814  basqtop  23829  qtopcld  23831  qtopeu  23834  qtoprest  23835  imastopn  23838  hmeontr  23887  hmeoimaf1o  23888  cmphaushmeo  23918  ordthmeolem  23919  elfm3  24068  rnelfmlem  24070  rnelfm  24071  alexsubALTlem4  24168  cldsubg  24229  tgpconncompeqg  24230  tgpconncomp  24231  qustgpopn  24238  qustgplem  24239  tsmsf1o  24263  ucncn  24402  imasf1oxms  24607  blcld  24623  metustfbas  24675  cfilucfil  24677  metuel2  24683  icchmeo  25061  relcmpcmet  25438  minveclem4a  25550  nulmbl2  25656  icombl  25684  ioombl  25685  uniiccdif  25698  volivth  25727  mbfres2  25765  itg1addlem5  25820  itgsplitioo  25958  dvcobr  26066  dvcnvlem  26096  lhop1lem  26133  lhop  26136  dvcnvrelem2  26138  uc1pval  26258  mon1pval  26260  vieta1lem2  26433  basellem5  27207  onnolt  28417  f1otrg  29129  axlowdimlem13  29213  axcontlem10  29232  uhgrspansubgr  29550  vtxdun  29740  pthdlem1  30024  eucrct2eupth  30505  ssmd1  32572  mdslj2i  32581  atcvat4i  32658  imadifxp  32856  nfpconfp  32889  2ndresdju  32906  ofpreima  32922  ofpreima2  32923  fsuppcurry1  32981  fsuppcurry2  32982  indpreima  33098  indf1ofs  33099  ccatws1f1olast  33185  gsumpart  33296  symgcom  33316  symgcom2  33317  pmtrcnel  33322  cycpmfvlem  33345  cycpmfv3  33348  elrgspnsubrunlem2  33481  elrspunidl  33652  idlinsubrg  33655  esplymhp  33875  esplyfval1  33880  esplyfvaln  33881  fldextrspunlsp  33981  qtophaus  34143  reff  34146  locfinreflem  34147  zarcmplem  34188  hauseqcn  34205  oms0  34604  eulerpartlemv  34671  eulerpartlemb  34675  eulerpartlemr  34681  eulerpartlemgs2  34687  eulerpartlemn  34688  ballotlemro  34830  bnj1253  35322  bnj1280  35325  onvfowev  35471  pthhashvtx  35491  acycgr0v  35511  prclisacycgr  35514  subfacp1lem3  35545  cvmscld  35636  cvmsss2  35637  cvmliftmolem1  35644  cvmliftlem7  35654  cvmlift2lem9  35674  cvmlift3lem7  35688  fnessref  36730  tailf  36748  poimirlem3  38134  mbfresfi  38177  cnambfre  38179  itg2addnclem2  38183  mettrifi  38268  ismtyres  38319  isdrngo2  38469  press  39010  diaintclN  41694  dibintclN  41803  dihintcl  41980  dochocss  42002  mapdunirnN  42286  pw2f1ocnv  43626  wessf1ornlem  45761  monoord2xrv  46055  itgcoscmulx  46541  ibliooicc  46543  stoweidlem11  46583  stoweidlem34  46606  fourierdlem48  46726  fourierdlem49  46727  fourierdlem74  46752  uniimaprimaeqfv  47986  elsetpreimafvssdm  47990  fdivmptf  49172  refdivmptf  49173  iscnrm3llem2  49579  imaidfu  49739