Theorem sseqtrrdi 3977

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

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3921

This theorem is referenced by:  3sstr4g  3989  abssdv  4020  disjxiun  5096  knatar  7337  iunpw  7750  fviunfun  7922  frrlem8  8269  frrlem10  8271  frrlem12  8273  frrlem14  8275  fprresex  8286  tfrlem9  8351  tfrlem9a  8352  tfrlem13  8356  tz7.44-2  8373  tz7.44-3  8374  tz7.49  8411  naddcllem  8641  naddov2  8644  naddasslem1  8660  naddasslem2  8661  marypha1lem  9376  ordtypelem2  9464  ixpiunwdom  9535  oemapvali  9636  tcss  9694  tcel  9695  pwwf  9762  rankpwi  9778  rankval3b  9781  cplem1  9844  dfac12lem2  10098  infmap2  10170  ackbij1b  10191  ttukeylem6  10468  fpwwe2lem10  10595  fpwwe2lem11  10596  fpwwe2lem12  10597  fpwwe2  10598  uznnssnn  12893  pfxccatpfx2  14747  shftfval  15080  rexuzre  15363  climsup  15680  clim2prod  15901  fprodntriv  15955  eulerthlem2  16800  ramtlecl  17019  mreexexlem4d  17662  mreexdomd  17664  gsumpropd2lem  18696  gsumzaddlem  19944  gsum2d  19995  telgsums  20016  pgpfac1lem1  20099  pgpfac1lem3a  20101  pgpfac1lem3  20102  pgpfac1lem5  20104  lspsolvlem  21192  lbsextlem2  21209  dsmmacl  21773  eltopss  22947  difopn  23074  tgrest  23199  perfopn  23225  pnfnei  23260  mnfnei  23261  regsep2  23416  cncmp  23432  uncmp  23443  hauscmplem  23446  hauscmp  23447  conndisj  23456  cnconn  23462  conncompss  23473  2ndcctbss  23495  islly2  23524  comppfsc  23572  1stckgenlem  23593  txuni2  23605  ptbasfi  23621  ptpjopn  23652  txindis  23674  txtube  23680  hausdiag  23685  xkoinjcn  23727  tgqtop  23752  filconn  23923  elfm2  23988  flimclslem  24024  flffbas  24035  fclsbas  24061  flimfnfcls  24068  alexsubALT  24091  symgtgp  24146  ustssco  24255  isucn2  24318  ucnima  24320  ucnprima  24321  blcls  24546  prdsxmslem2  24569  isngp2  24637  tgioo  24836  xrtgioo  24847  xrsmopn  24853  opnreen  24872  cnheiborlem  24996  cnllycmp  24998  tcphcph  25279  rrxmvallem  25446  uniioombllem4  25628  dyadmbllem  25641  opnmbllem  25643  mbfimaopnlem  25697  mbflimsup  25708  i1fadd  25737  i1fmul  25738  itg1addlem4  25741  i1fmulc  25745  limciun  25936  dvlip2  26037  c1lip3  26041  lhop  26058  dvfsumlem2  26069  dvfsumrlimge0  26072  dvfsumrlim2  26074  ulmval  26420  psercnlem2  26464  efopnlem2  26699  efopn  26700  madebdayim  27958  madefi  27983  oldfi  27984  addbdaylem  28087  oniso  28341  oldfib  28447  umgrres1lem  29457  upgrres1  29460  nbgrssvwo2  29509  ubthlem1  31019  issh2  31358  mdsymlem1  32552  iunxpssiun1  32717  padct  32870  xrofsup  32919  fz2ssnn0  32937  ccatws1f1o  33090  elrgspnlem1  33384  unitpidl1  33571  mxidlirred  33621  zarclsint  34130  tpr2rico  34170  sibfinima  34597  fct2relem  34855  bnj906  35189  bnj1014  35220  bnj1286  35278  bnj1408  35295  bnj1450  35309  bnj1452  35311  bnj1498  35320  bnj1501  35326  vonf1oonfo  35422  lfuhgr  35432  cvmopnlem  35592  cvmfolem  35593  cvmliftlem6  35604  cvmliftlem8  35606  cvmliftlem13  35610  cvmliftlem15  35612  cvmlift2lem9  35625  cvmlift2lem11  35627  cvmlift2lem12  35628  mclsppslem  35897  filnetlem4  36705  dissneqlem  37798  pibt2  37875  lindsdom  38077  opnmbllem0  38119  cnambfre  38131  heibor1lem  38272  osumcllem1N  40544  osumcllem2N  40545  pexmidlem6N  40563  dochexmidlem6  42053  dochexmidlem7  42054  mapdrvallem3  42234  evlsmhpvvval  43141  naddwordnexlem4  43942  k0004ss2  44692  cpcolld  44798  dvsconst  44870  dvsid  44871  dvsef  44872  iunconnlem2  45474  uzssd2  45955  climinf  46146  climsuse  46148  climresmpt  46197  climleltrp  46214  stoweidlem28  46566  stoweidlem50  46588  stoweidlem52  46590  stoweidlem53  46591  stoweidlem54  46592  fourierdlem54  46698  fourierdlem80  46724  meaiininclem  47024  caratheodorylem2  47065  hspmbllem2  47165  mbfresmf  47277  smfmbfcex  47298  smflimlem2  47310  smflimsuplem2  47359  smflimsuplem3  47360  smflimsuplem5  47362  smflimsuplem6  47363  gpgedgvtx1lem  47893  isuspgrim0  48480  gpgusgralem  48642  upgredgssspr  48729  setrec1  50276  setrecsres  50287  aacllem  50386