Theorem sseqtrrdi 3979

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

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

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 2701

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

This theorem is referenced by:  3sstr4g  3991  abssdv  4022  disjxiun  5092  knatar  7298  iunpw  7711  fviunfun  7887  frrlem8  8233  frrlem10  8235  frrlem12  8237  frrlem14  8239  fprresex  8250  tfrlem9  8314  tfrlem9a  8315  tfrlem13  8319  tz7.44-2  8336  tz7.44-3  8337  tz7.49  8374  naddcllem  8601  naddov2  8604  naddasslem1  8619  naddasslem2  8620  marypha1lem  9342  ordtypelem2  9430  ixpiunwdom  9501  oemapvali  9599  tcss  9659  tcel  9660  pwwf  9722  rankpwi  9738  rankval3b  9741  cplem1  9804  dfac12lem2  10058  infmap2  10130  ackbij1b  10151  ttukeylem6  10427  fpwwe2lem10  10553  fpwwe2lem11  10554  fpwwe2lem12  10555  fpwwe2  10556  uznnssnn  12814  pfxccatpfx2  14661  shftfval  14995  rexuzre  15278  climsup  15595  clim2prod  15813  fprodntriv  15867  eulerthlem2  16711  ramtlecl  16930  mreexexlem4d  17571  mreexdomd  17573  gsumpropd2lem  18571  gsumzaddlem  19818  gsum2d  19869  telgsums  19890  pgpfac1lem1  19973  pgpfac1lem3a  19975  pgpfac1lem3  19976  pgpfac1lem5  19978  lspsolvlem  21067  lbsextlem2  21084  dsmmacl  21666  eltopss  22810  difopn  22937  tgrest  23062  perfopn  23088  pnfnei  23123  mnfnei  23124  regsep2  23279  cncmp  23295  uncmp  23306  hauscmplem  23309  hauscmp  23310  conndisj  23319  cnconn  23325  conncompss  23336  2ndcctbss  23358  islly2  23387  comppfsc  23435  1stckgenlem  23456  txuni2  23468  ptbasfi  23484  ptpjopn  23515  txindis  23537  txtube  23543  hausdiag  23548  xkoinjcn  23590  tgqtop  23615  filconn  23786  elfm2  23851  flimclslem  23887  flffbas  23898  fclsbas  23924  flimfnfcls  23931  alexsubALT  23954  symgtgp  24009  ustssco  24118  isucn2  24182  ucnima  24184  ucnprima  24185  blcls  24410  prdsxmslem2  24433  isngp2  24501  tgioo  24700  xrtgioo  24711  xrsmopn  24717  opnreen  24736  cnheiborlem  24869  cnllycmp  24871  tcphcph  25153  rrxmvallem  25320  uniioombllem4  25503  dyadmbllem  25516  opnmbllem  25518  mbfimaopnlem  25572  mbflimsup  25583  i1fadd  25612  i1fmul  25613  itg1addlem4  25616  i1fmulc  25620  limciun  25811  dvlip2  25916  c1lip3  25920  lhop  25937  dvfsumlem2  25949  dvfsumlem2OLD  25950  dvfsumrlimge0  25953  dvfsumrlim2  25955  ulmval  26305  psercnlem2  26350  efopnlem2  26582  efopn  26583  madebdayim  27820  madefi  27845  oldfi  27846  addsbdaylem  27946  onsiso  28192  umgrres1lem  29273  upgrres1  29276  nbgrssvwo2  29325  ubthlem1  30832  issh2  31171  mdsymlem1  32365  iunxpssiun1  32530  padct  32676  xrofsup  32723  fz2ssnn0  32741  ccatws1f1o  32906  elrgspnlem1  33192  unitpidl1  33371  mxidlirred  33419  zarclsint  33838  tpr2rico  33878  sibfinima  34306  fct2relem  34564  bnj906  34896  bnj1014  34927  bnj1286  34985  bnj1408  35002  bnj1450  35016  bnj1452  35018  bnj1498  35027  bnj1501  35033  lfuhgr  35090  cvmopnlem  35250  cvmfolem  35251  cvmliftlem6  35262  cvmliftlem8  35264  cvmliftlem13  35268  cvmliftlem15  35270  cvmlift2lem9  35283  cvmlift2lem11  35285  cvmlift2lem12  35286  mclsppslem  35555  filnetlem4  36354  dissneqlem  37313  pibt2  37390  lindsdom  37593  opnmbllem0  37635  cnambfre  37647  heibor1lem  37788  osumcllem1N  39935  osumcllem2N  39936  pexmidlem6N  39954  dochexmidlem6  41444  dochexmidlem7  41445  mapdrvallem3  41625  evlsmhpvvval  42568  naddwordnexlem4  43374  k0004ss2  44125  cpcolld  44231  dvsconst  44303  dvsid  44304  dvsef  44305  iunconnlem2  44908  uzssd2  45397  climinf  45588  climsuse  45590  climresmpt  45641  climleltrp  45658  stoweidlem28  46010  stoweidlem50  46032  stoweidlem52  46034  stoweidlem53  46035  stoweidlem54  46036  fourierdlem54  46142  fourierdlem80  46168  meaiininclem  46468  caratheodorylem2  46509  hspmbllem2  46609  mbfresmf  46721  smfmbfcex  46742  smflimlem2  46754  smflimsuplem2  46803  smflimsuplem3  46804  smflimsuplem5  46806  smflimsuplem6  46807  gpgedgvtx1lem  47316  isuspgrim0  47879  gpgusgralem  48041  upgredgssspr  48128  setrec1  49677  setrecsres  49688  aacllem  49787