Theorem sseqtrrdi 3963

Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
sseqtrrdi.1	⊢ (𝜑 → 𝐴 ⊆ 𝐵)
sseqtrrdi.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
sseqtrrdi	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem sseqtrrdi

Step	Hyp	Ref	Expression
1		sseqtrrdi.1	. 2 ⊢ (𝜑 → 𝐴 ⊆ 𝐵)
2		sseqtrrdi.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2749	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtrdi 3962	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2732  df-ss 3907

This theorem is referenced by:  3sstr4g  3975  abssdv  4005  disjxiun  5076  knatar  7308  iunpw  7721  fviunfun  7894  frrlem8  8240  frrlem10  8242  frrlem12  8244  frrlem14  8246  fprresex  8257  tfrlem9  8321  tfrlem9a  8322  tfrlem13  8326  tz7.44-2  8343  tz7.44-3  8344  tz7.49  8381  naddcllem  8609  naddov2  8612  naddasslem1  8627  naddasslem2  8628  marypha1lem  9343  ordtypelem2  9431  ixpiunwdom  9502  oemapvali  9603  tcss  9661  tcel  9662  pwwf  9729  rankpwi  9745  rankval3b  9748  cplem1  9811  dfac12lem2  10065  infmap2  10137  ackbij1b  10158  ttukeylem6  10434  fpwwe2lem10  10561  fpwwe2lem11  10562  fpwwe2lem12  10563  fpwwe2  10564  uznnssnn  12843  pfxccatpfx2  14697  shftfval  15030  rexuzre  15313  climsup  15630  clim2prod  15851  fprodntriv  15905  eulerthlem2  16750  ramtlecl  16969  mreexexlem4d  17611  mreexdomd  17613  gsumpropd2lem  18645  gsumzaddlem  19894  gsum2d  19945  telgsums  19966  pgpfac1lem1  20049  pgpfac1lem3a  20051  pgpfac1lem3  20052  pgpfac1lem5  20054  lspsolvlem  21142  lbsextlem2  21159  dsmmacl  21723  eltopss  22897  difopn  23024  tgrest  23149  perfopn  23175  pnfnei  23210  mnfnei  23211  regsep2  23366  cncmp  23382  uncmp  23393  hauscmplem  23396  hauscmp  23397  conndisj  23406  cnconn  23412  conncompss  23423  2ndcctbss  23445  islly2  23474  comppfsc  23522  1stckgenlem  23543  txuni2  23555  ptbasfi  23571  ptpjopn  23602  txindis  23624  txtube  23630  hausdiag  23635  xkoinjcn  23677  tgqtop  23702  filconn  23873  elfm2  23938  flimclslem  23974  flffbas  23985  fclsbas  24011  flimfnfcls  24018  alexsubALT  24041  symgtgp  24096  ustssco  24205  isucn2  24268  ucnima  24270  ucnprima  24271  blcls  24496  prdsxmslem2  24519  isngp2  24587  tgioo  24786  xrtgioo  24797  xrsmopn  24803  opnreen  24822  cnheiborlem  24946  cnllycmp  24948  tcphcph  25229  rrxmvallem  25396  uniioombllem4  25578  dyadmbllem  25591  opnmbllem  25593  mbfimaopnlem  25647  mbflimsup  25658  i1fadd  25687  i1fmul  25688  itg1addlem4  25691  i1fmulc  25695  limciun  25886  dvlip2  25987  c1lip3  25991  lhop  26008  dvfsumlem2  26019  dvfsumrlimge0  26022  dvfsumrlim2  26024  ulmval  26370  psercnlem2  26414  efopnlem2  26646  efopn  26647  madebdayim  27905  madefi  27930  oldfi  27931  addbdaylem  28034  oniso  28288  oldfib  28394  umgrres1lem  29404  upgrres1  29407  nbgrssvwo2  29456  ubthlem1  30966  issh2  31305  mdsymlem1  32499  iunxpssiun1  32664  padct  32817  xrofsup  32866  fz2ssnn0  32884  ccatws1f1o  33037  elrgspnlem1  33330  unitpidl1  33514  mxidlirred  33562  zarclsint  34063  tpr2rico  34103  sibfinima  34530  fct2relem  34788  bnj906  35119  bnj1014  35150  bnj1286  35208  bnj1408  35225  bnj1450  35239  bnj1452  35241  bnj1498  35250  bnj1501  35256  lfuhgr  35353  cvmopnlem  35513  cvmfolem  35514  cvmliftlem6  35525  cvmliftlem8  35527  cvmliftlem13  35531  cvmliftlem15  35533  cvmlift2lem9  35546  cvmlift2lem11  35548  cvmlift2lem12  35549  mclsppslem  35818  filnetlem4  36616  dissneqlem  37709  pibt2  37786  lindsdom  37988  opnmbllem0  38030  cnambfre  38042  heibor1lem  38183  osumcllem1N  40455  osumcllem2N  40456  pexmidlem6N  40474  dochexmidlem6  41964  dochexmidlem7  41965  mapdrvallem3  42145  evlsmhpvvval  43052  naddwordnexlem4  43853  k0004ss2  44603  cpcolld  44709  dvsconst  44781  dvsid  44782  dvsef  44783  iunconnlem2  45385  uzssd2  45867  climinf  46058  climsuse  46060  climresmpt  46109  climleltrp  46126  stoweidlem28  46478  stoweidlem50  46500  stoweidlem52  46502  stoweidlem53  46503  stoweidlem54  46504  fourierdlem54  46610  fourierdlem80  46636  meaiininclem  46936  caratheodorylem2  46977  hspmbllem2  47077  mbfresmf  47189  smfmbfcex  47210  smflimlem2  47222  smflimsuplem2  47271  smflimsuplem3  47272  smflimsuplem5  47274  smflimsuplem6  47275  gpgedgvtx1lem  47805  isuspgrim0  48392  gpgusgralem  48554  upgredgssspr  48641  setrec1  50188  setrecsres  50199  aacllem  50298