Theorem sseqtrrdi 3991

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3917

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2722  df-ss 3934

This theorem is referenced by:  3sstr4g  4003  abssdv  4034  disjxiun  5107  knatar  7335  iunpw  7750  fviunfun  7926  frrlem8  8275  frrlem10  8277  frrlem12  8279  frrlem14  8281  fprresex  8292  tfrlem9  8356  tfrlem9a  8357  tfrlem13  8361  tz7.44-2  8378  tz7.44-3  8379  tz7.49  8416  naddcllem  8643  naddov2  8646  naddasslem1  8661  naddasslem2  8662  marypha1lem  9391  ordtypelem2  9479  ixpiunwdom  9550  oemapvali  9644  tcss  9704  tcel  9705  pwwf  9767  rankpwi  9783  rankval3b  9786  cplem1  9849  dfac12lem2  10105  infmap2  10177  ackbij1b  10198  ttukeylem6  10474  fpwwe2lem10  10600  fpwwe2lem11  10601  fpwwe2lem12  10602  fpwwe2  10603  uznnssnn  12861  pfxccatpfx2  14709  shftfval  15043  rexuzre  15326  climsup  15643  clim2prod  15861  fprodntriv  15915  eulerthlem2  16759  ramtlecl  16978  mreexexlem4d  17615  mreexdomd  17617  gsumpropd2lem  18613  gsumzaddlem  19858  gsum2d  19909  telgsums  19930  pgpfac1lem1  20013  pgpfac1lem3a  20015  pgpfac1lem3  20016  pgpfac1lem5  20018  lspsolvlem  21059  lbsextlem2  21076  dsmmacl  21657  eltopss  22801  difopn  22928  tgrest  23053  perfopn  23079  pnfnei  23114  mnfnei  23115  regsep2  23270  cncmp  23286  uncmp  23297  hauscmplem  23300  hauscmp  23301  conndisj  23310  cnconn  23316  conncompss  23327  2ndcctbss  23349  islly2  23378  comppfsc  23426  1stckgenlem  23447  txuni2  23459  ptbasfi  23475  ptpjopn  23506  txindis  23528  txtube  23534  hausdiag  23539  xkoinjcn  23581  tgqtop  23606  filconn  23777  elfm2  23842  flimclslem  23878  flffbas  23889  fclsbas  23915  flimfnfcls  23922  alexsubALT  23945  symgtgp  24000  ustssco  24109  isucn2  24173  ucnima  24175  ucnprima  24176  blcls  24401  prdsxmslem2  24424  isngp2  24492  tgioo  24691  xrtgioo  24702  xrsmopn  24708  opnreen  24727  cnheiborlem  24860  cnllycmp  24862  tcphcph  25144  rrxmvallem  25311  uniioombllem4  25494  dyadmbllem  25507  opnmbllem  25509  mbfimaopnlem  25563  mbflimsup  25574  i1fadd  25603  i1fmul  25604  itg1addlem4  25607  i1fmulc  25611  limciun  25802  dvlip2  25907  c1lip3  25911  lhop  25928  dvfsumlem2  25940  dvfsumlem2OLD  25941  dvfsumrlimge0  25944  dvfsumrlim2  25946  ulmval  26296  psercnlem2  26341  efopnlem2  26573  efopn  26574  madebdayim  27806  madefi  27831  oldfi  27832  addsbdaylem  27930  onsiso  28176  umgrres1lem  29244  upgrres1  29247  nbgrssvwo2  29296  ubthlem1  30806  issh2  31145  mdsymlem1  32339  iunxpssiun1  32504  padct  32650  xrofsup  32697  fz2ssnn0  32715  ccatws1f1o  32880  elrgspnlem1  33200  unitpidl1  33402  mxidlirred  33450  zarclsint  33869  tpr2rico  33909  sibfinima  34337  fct2relem  34595  bnj906  34927  bnj1014  34958  bnj1286  35016  bnj1408  35033  bnj1450  35047  bnj1452  35049  bnj1498  35058  bnj1501  35064  lfuhgr  35112  cvmopnlem  35272  cvmfolem  35273  cvmliftlem6  35284  cvmliftlem8  35286  cvmliftlem13  35290  cvmliftlem15  35292  cvmlift2lem9  35305  cvmlift2lem11  35307  cvmlift2lem12  35308  mclsppslem  35577  filnetlem4  36376  dissneqlem  37335  pibt2  37412  lindsdom  37615  opnmbllem0  37657  cnambfre  37669  heibor1lem  37810  osumcllem1N  39957  osumcllem2N  39958  pexmidlem6N  39976  dochexmidlem6  41466  dochexmidlem7  41467  mapdrvallem3  41647  evlsmhpvvval  42590  naddwordnexlem4  43397  k0004ss2  44148  cpcolld  44254  dvsconst  44326  dvsid  44327  dvsef  44328  iunconnlem2  44931  uzssd2  45420  climinf  45611  climsuse  45613  climresmpt  45664  climleltrp  45681  stoweidlem28  46033  stoweidlem50  46055  stoweidlem52  46057  stoweidlem53  46058  stoweidlem54  46059  fourierdlem54  46165  fourierdlem80  46191  meaiininclem  46491  caratheodorylem2  46532  hspmbllem2  46632  mbfresmf  46744  smfmbfcex  46765  smflimlem2  46777  smflimsuplem2  46826  smflimsuplem3  46827  smflimsuplem5  46829  smflimsuplem6  46830  gpgedgvtx1lem  47336  isuspgrim0  47898  gpgusgralem  48051  upgredgssspr  48135  setrec1  49684  setrecsres  49695  aacllem  49794