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  7303  iunpw  7716  fviunfun  7889  frrlem8  8234  frrlem10  8236  frrlem12  8238  frrlem14  8240  fprresex  8251  tfrlem9  8315  tfrlem9a  8316  tfrlem13  8320  tz7.44-2  8337  tz7.44-3  8338  tz7.49  8375  naddcllem  8603  naddov2  8606  naddasslem1  8621  naddasslem2  8622  marypha1lem  9337  ordtypelem2  9425  ixpiunwdom  9496  oemapvali  9594  tcss  9652  tcel  9653  pwwf  9720  rankpwi  9736  rankval3b  9739  cplem1  9802  dfac12lem2  10056  infmap2  10128  ackbij1b  10149  ttukeylem6  10425  fpwwe2lem10  10552  fpwwe2lem11  10553  fpwwe2lem12  10554  fpwwe2  10555  uznnssnn  12834  pfxccatpfx2  14688  shftfval  15021  rexuzre  15304  climsup  15621  clim2prod  15842  fprodntriv  15896  eulerthlem2  16741  ramtlecl  16960  mreexexlem4d  17602  mreexdomd  17604  gsumpropd2lem  18636  gsumzaddlem  19885  gsum2d  19936  telgsums  19957  pgpfac1lem1  20040  pgpfac1lem3a  20042  pgpfac1lem3  20043  pgpfac1lem5  20045  lspsolvlem  21130  lbsextlem2  21147  dsmmacl  21729  eltopss  22881  difopn  23008  tgrest  23133  perfopn  23159  pnfnei  23194  mnfnei  23195  regsep2  23350  cncmp  23366  uncmp  23377  hauscmplem  23380  hauscmp  23381  conndisj  23390  cnconn  23396  conncompss  23407  2ndcctbss  23429  islly2  23458  comppfsc  23506  1stckgenlem  23527  txuni2  23539  ptbasfi  23555  ptpjopn  23586  txindis  23608  txtube  23614  hausdiag  23619  xkoinjcn  23661  tgqtop  23686  filconn  23857  elfm2  23922  flimclslem  23958  flffbas  23969  fclsbas  23995  flimfnfcls  24002  alexsubALT  24025  symgtgp  24080  ustssco  24189  isucn2  24252  ucnima  24254  ucnprima  24255  blcls  24480  prdsxmslem2  24503  isngp2  24571  tgioo  24770  xrtgioo  24781  xrsmopn  24787  opnreen  24806  cnheiborlem  24930  cnllycmp  24932  tcphcph  25213  rrxmvallem  25380  uniioombllem4  25562  dyadmbllem  25575  opnmbllem  25577  mbfimaopnlem  25631  mbflimsup  25642  i1fadd  25671  i1fmul  25672  itg1addlem4  25675  i1fmulc  25679  limciun  25870  dvlip2  25972  c1lip3  25976  lhop  25993  dvfsumlem2  26005  dvfsumlem2OLD  26006  dvfsumrlimge0  26009  dvfsumrlim2  26011  ulmval  26360  psercnlem2  26405  efopnlem2  26637  efopn  26638  madebdayim  27899  madefi  27924  oldfi  27925  addbdaylem  28028  oniso  28282  oldfib  28388  umgrres1lem  29398  upgrres1  29401  nbgrssvwo2  29450  ubthlem1  30961  issh2  31300  mdsymlem1  32494  iunxpssiun1  32658  padct  32811  xrofsup  32860  fz2ssnn0  32878  ccatws1f1o  33031  elrgspnlem1  33323  unitpidl1  33504  mxidlirred  33552  zarclsint  34037  tpr2rico  34077  sibfinima  34504  fct2relem  34762  bnj906  35093  bnj1014  35124  bnj1286  35182  bnj1408  35199  bnj1450  35213  bnj1452  35215  bnj1498  35224  bnj1501  35230  lfuhgr  35321  cvmopnlem  35481  cvmfolem  35482  cvmliftlem6  35493  cvmliftlem8  35495  cvmliftlem13  35499  cvmliftlem15  35501  cvmlift2lem9  35514  cvmlift2lem11  35516  cvmlift2lem12  35517  mclsppslem  35786  filnetlem4  36584  dissneqlem  37667  pibt2  37744  lindsdom  37946  opnmbllem0  37988  cnambfre  38000  heibor1lem  38141  osumcllem1N  40413  osumcllem2N  40414  pexmidlem6N  40432  dochexmidlem6  41922  dochexmidlem7  41923  mapdrvallem3  42103  evlsmhpvvval  43039  naddwordnexlem4  43844  k0004ss2  44594  cpcolld  44700  dvsconst  44772  dvsid  44773  dvsef  44774  iunconnlem2  45376  uzssd2  45860  climinf  46051  climsuse  46053  climresmpt  46102  climleltrp  46119  stoweidlem28  46471  stoweidlem50  46493  stoweidlem52  46495  stoweidlem53  46496  stoweidlem54  46497  fourierdlem54  46603  fourierdlem80  46629  meaiininclem  46929  caratheodorylem2  46970  hspmbllem2  47070  mbfresmf  47182  smfmbfcex  47203  smflimlem2  47215  smflimsuplem2  47264  smflimsuplem3  47265  smflimsuplem5  47267  smflimsuplem6  47268  gpgedgvtx1lem  47780  isuspgrim0  48367  gpgusgralem  48529  upgredgssspr  48616  setrec1  50163  setrecsres  50174  aacllem  50273