Theorem sseqtrrdi 3964

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3907

This theorem is referenced by:  3sstr4g  3976  abssdv  4008  disjxiun  5083  knatar  7305  iunpw  7718  fviunfun  7891  frrlem8  8236  frrlem10  8238  frrlem12  8240  frrlem14  8242  fprresex  8253  tfrlem9  8317  tfrlem9a  8318  tfrlem13  8322  tz7.44-2  8339  tz7.44-3  8340  tz7.49  8377  naddcllem  8605  naddov2  8608  naddasslem1  8623  naddasslem2  8624  marypha1lem  9339  ordtypelem2  9427  ixpiunwdom  9498  oemapvali  9596  tcss  9654  tcel  9655  pwwf  9722  rankpwi  9738  rankval3b  9741  cplem1  9804  dfac12lem2  10058  infmap2  10130  ackbij1b  10151  ttukeylem6  10427  fpwwe2lem10  10554  fpwwe2lem11  10555  fpwwe2lem12  10556  fpwwe2  10557  uznnssnn  12836  pfxccatpfx2  14690  shftfval  15023  rexuzre  15306  climsup  15623  clim2prod  15844  fprodntriv  15898  eulerthlem2  16743  ramtlecl  16962  mreexexlem4d  17604  mreexdomd  17606  gsumpropd2lem  18638  gsumzaddlem  19887  gsum2d  19938  telgsums  19959  pgpfac1lem1  20042  pgpfac1lem3a  20044  pgpfac1lem3  20045  pgpfac1lem5  20047  lspsolvlem  21132  lbsextlem2  21149  dsmmacl  21731  eltopss  22882  difopn  23009  tgrest  23134  perfopn  23160  pnfnei  23195  mnfnei  23196  regsep2  23351  cncmp  23367  uncmp  23378  hauscmplem  23381  hauscmp  23382  conndisj  23391  cnconn  23397  conncompss  23408  2ndcctbss  23430  islly2  23459  comppfsc  23507  1stckgenlem  23528  txuni2  23540  ptbasfi  23556  ptpjopn  23587  txindis  23609  txtube  23615  hausdiag  23620  xkoinjcn  23662  tgqtop  23687  filconn  23858  elfm2  23923  flimclslem  23959  flffbas  23970  fclsbas  23996  flimfnfcls  24003  alexsubALT  24026  symgtgp  24081  ustssco  24190  isucn2  24253  ucnima  24255  ucnprima  24256  blcls  24481  prdsxmslem2  24504  isngp2  24572  tgioo  24771  xrtgioo  24782  xrsmopn  24788  opnreen  24807  cnheiborlem  24931  cnllycmp  24933  tcphcph  25214  rrxmvallem  25381  uniioombllem4  25563  dyadmbllem  25576  opnmbllem  25578  mbfimaopnlem  25632  mbflimsup  25643  i1fadd  25672  i1fmul  25673  itg1addlem4  25676  i1fmulc  25680  limciun  25871  dvlip2  25972  c1lip3  25976  lhop  25993  dvfsumlem2  26004  dvfsumrlimge0  26007  dvfsumrlim2  26009  ulmval  26358  psercnlem2  26402  efopnlem2  26634  efopn  26635  madebdayim  27894  madefi  27919  oldfi  27920  addbdaylem  28023  oniso  28277  oldfib  28383  umgrres1lem  29393  upgrres1  29396  nbgrssvwo2  29445  ubthlem1  30956  issh2  31295  mdsymlem1  32489  iunxpssiun1  32653  padct  32806  xrofsup  32855  fz2ssnn0  32873  ccatws1f1o  33026  elrgspnlem1  33318  unitpidl1  33499  mxidlirred  33547  zarclsint  34032  tpr2rico  34072  sibfinima  34499  fct2relem  34757  bnj906  35088  bnj1014  35119  bnj1286  35177  bnj1408  35194  bnj1450  35208  bnj1452  35210  bnj1498  35219  bnj1501  35225  lfuhgr  35316  cvmopnlem  35476  cvmfolem  35477  cvmliftlem6  35488  cvmliftlem8  35490  cvmliftlem13  35494  cvmliftlem15  35496  cvmlift2lem9  35509  cvmlift2lem11  35511  cvmlift2lem12  35512  mclsppslem  35781  filnetlem4  36579  dissneqlem  37670  pibt2  37747  lindsdom  37949  opnmbllem0  37991  cnambfre  38003  heibor1lem  38144  osumcllem1N  40416  osumcllem2N  40417  pexmidlem6N  40435  dochexmidlem6  41925  dochexmidlem7  41926  mapdrvallem3  42106  evlsmhpvvval  43042  naddwordnexlem4  43847  k0004ss2  44597  cpcolld  44703  dvsconst  44775  dvsid  44776  dvsef  44777  iunconnlem2  45379  uzssd2  45863  climinf  46054  climsuse  46056  climresmpt  46105  climleltrp  46122  stoweidlem28  46474  stoweidlem50  46496  stoweidlem52  46498  stoweidlem53  46499  stoweidlem54  46500  fourierdlem54  46606  fourierdlem80  46632  meaiininclem  46932  caratheodorylem2  46973  hspmbllem2  47073  mbfresmf  47185  smfmbfcex  47206  smflimlem2  47218  smflimsuplem2  47267  smflimsuplem3  47268  smflimsuplem5  47270  smflimsuplem6  47271  gpgedgvtx1lem  47795  isuspgrim0  48382  gpgusgralem  48544  upgredgssspr  48631  setrec1  50178  setrecsres  50189  aacllem  50288