Theorem sseqtrrdi 4005

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 2743	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	sseqtrdi 4004	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ss 3948

This theorem is referenced by:  3sstr4g  4017  abssdv  4048  disjxiun  5120  knatar  7359  iunpw  7773  fviunfun  7951  frrlem8  8300  frrlem10  8302  frrlem12  8304  frrlem14  8306  fprresex  8317  wfrdmclOLD  8339  wfrlem12OLD  8342  wfrlem16OLD  8346  wfrlem17OLD  8347  tfrlem9  8407  tfrlem9a  8408  tfrlem13  8412  tz7.44-2  8429  tz7.44-3  8430  tz7.49  8467  naddcllem  8696  naddov2  8699  naddasslem1  8714  naddasslem2  8715  marypha1lem  9455  ordtypelem2  9541  ixpiunwdom  9612  oemapvali  9706  tcss  9766  tcel  9767  pwwf  9829  rankpwi  9845  rankval3b  9848  cplem1  9911  dfac12lem2  10167  infmap2  10239  ackbij1b  10260  ttukeylem6  10536  fpwwe2lem10  10662  fpwwe2lem11  10663  fpwwe2lem12  10664  fpwwe2  10665  uznnssnn  12919  pfxccatpfx2  14757  shftfval  15091  rexuzre  15373  climsup  15688  clim2prod  15906  fprodntriv  15960  eulerthlem2  16801  ramtlecl  17020  mreexexlem4d  17661  mreexdomd  17663  gsumpropd2lem  18661  gsumzaddlem  19907  gsum2d  19958  telgsums  19979  pgpfac1lem1  20062  pgpfac1lem3a  20064  pgpfac1lem3  20065  pgpfac1lem5  20067  lspsolvlem  21112  lbsextlem2  21129  dsmmacl  21715  eltopss  22861  difopn  22988  tgrest  23113  perfopn  23139  pnfnei  23174  mnfnei  23175  regsep2  23330  cncmp  23346  uncmp  23357  hauscmplem  23360  hauscmp  23361  conndisj  23370  cnconn  23376  conncompss  23387  2ndcctbss  23409  islly2  23438  comppfsc  23486  1stckgenlem  23507  txuni2  23519  ptbasfi  23535  ptpjopn  23566  txindis  23588  txtube  23594  hausdiag  23599  xkoinjcn  23641  tgqtop  23666  filconn  23837  elfm2  23902  flimclslem  23938  flffbas  23949  fclsbas  23975  flimfnfcls  23982  alexsubALT  24005  symgtgp  24060  ustssco  24169  isucn2  24233  ucnima  24235  ucnprima  24236  blcls  24463  prdsxmslem2  24486  isngp2  24554  tgioo  24753  xrtgioo  24764  xrsmopn  24770  opnreen  24789  cnheiborlem  24922  cnllycmp  24924  tcphcph  25207  rrxmvallem  25374  uniioombllem4  25557  dyadmbllem  25570  opnmbllem  25572  mbfimaopnlem  25626  mbflimsup  25637  i1fadd  25666  i1fmul  25667  itg1addlem4  25670  i1fmulc  25674  limciun  25865  dvlip2  25970  c1lip3  25974  lhop  25991  dvfsumlem2  26003  dvfsumlem2OLD  26004  dvfsumrlimge0  26007  dvfsumrlim2  26009  ulmval  26359  psercnlem2  26404  efopnlem2  26635  efopn  26636  madebdayim  27862  madefi  27886  oldfi  27887  addsbdaylem  27985  umgrres1lem  29255  upgrres1  29258  nbgrssvwo2  29307  ubthlem1  30817  issh2  31156  mdsymlem1  32350  iunxpssiun1  32516  padct  32666  xrofsup  32708  fz2ssnn0  32726  ccatws1f1o  32876  elrgspnlem1  33185  unitpidl1  33387  mxidlirred  33435  zarclsint  33830  tpr2rico  33870  sibfinima  34300  fct2relem  34571  bnj906  34903  bnj1014  34934  bnj1286  34992  bnj1408  35009  bnj1450  35023  bnj1452  35025  bnj1498  35034  bnj1501  35040  lfuhgr  35082  cvmopnlem  35242  cvmfolem  35243  cvmliftlem6  35254  cvmliftlem8  35256  cvmliftlem13  35260  cvmliftlem15  35262  cvmlift2lem9  35275  cvmlift2lem11  35277  cvmlift2lem12  35278  mclsppslem  35547  filnetlem4  36341  dissneqlem  37300  pibt2  37377  lindsdom  37580  opnmbllem0  37622  cnambfre  37634  heibor1lem  37775  osumcllem1N  39917  osumcllem2N  39918  pexmidlem6N  39936  dochexmidlem6  41426  dochexmidlem7  41427  mapdrvallem3  41607  evlsmhpvvval  42568  naddwordnexlem4  43376  k0004ss2  44127  cpcolld  44234  dvsconst  44306  dvsid  44307  dvsef  44308  iunconnlem2  44912  uzssd2  45385  climinf  45578  climsuse  45580  climresmpt  45631  climleltrp  45648  stoweidlem28  46000  stoweidlem50  46022  stoweidlem52  46024  stoweidlem53  46025  stoweidlem54  46026  fourierdlem54  46132  fourierdlem80  46158  meaiininclem  46458  caratheodorylem2  46499  hspmbllem2  46599  mbfresmf  46711  smfmbfcex  46732  smflimlem2  46744  smflimsuplem2  46793  smflimsuplem3  46794  smflimsuplem5  46796  smflimsuplem6  46797  isuspgrim0  47830  gpgusgralem  47969  gpgedgvtx1lem  47975  upgredgssspr  48017  setrec1  49218  setrecsres  49229  aacllem  49328