Theorem sseqtrrdi 3968

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  disjxiun  5067  knatar  7208  iunpw  7599  fviunfun  7761  frrlem8  8080  frrlem10  8082  frrlem12  8084  frrlem14  8086  fprresex  8097  wfrdmclOLD  8119  wfrlem12OLD  8122  wfrlem16OLD  8126  wfrlem17OLD  8127  tfrlem9  8187  tfrlem9a  8188  tfrlem13  8192  tz7.44-2  8209  tz7.44-3  8210  tz7.49  8246  marypha1lem  9122  ordtypelem2  9208  ixpiunwdom  9279  oemapvali  9372  trpredpred  9406  trpredtr  9408  trpredrec  9415  tcss  9433  tcel  9434  pwwf  9496  rankpwi  9512  rankval3b  9515  cplem1  9578  dfac12lem2  9831  infmap2  9905  ackbij1b  9926  ttukeylem6  10201  fpwwe2lem10  10327  fpwwe2lem11  10328  fpwwe2lem12  10329  fpwwe2  10330  uznnssnn  12564  pfxccatpfx2  14378  shftfval  14709  rexuzre  14992  climsup  15309  clim2prod  15528  fprodntriv  15580  eulerthlem2  16411  ramtlecl  16629  mreexexlem4d  17273  mreexdomd  17275  gsumpropd2lem  18278  gsumzaddlem  19437  gsum2d  19488  telgsums  19509  pgpfac1lem1  19592  pgpfac1lem3a  19594  pgpfac1lem3  19595  pgpfac1lem5  19597  lspsolvlem  20319  lbsextlem2  20336  dsmmacl  20858  eltopss  21964  difopn  22093  tgrest  22218  perfopn  22244  pnfnei  22279  mnfnei  22280  regsep2  22435  cncmp  22451  uncmp  22462  hauscmplem  22465  hauscmp  22466  conndisj  22475  cnconn  22481  conncompss  22492  2ndcctbss  22514  islly2  22543  comppfsc  22591  1stckgenlem  22612  txuni2  22624  ptbasfi  22640  ptpjopn  22671  txindis  22693  txtube  22699  hausdiag  22704  xkoinjcn  22746  tgqtop  22771  filconn  22942  elfm2  23007  flimclslem  23043  flffbas  23054  fclsbas  23080  flimfnfcls  23087  alexsubALT  23110  symgtgp  23165  ustssco  23274  isucn2  23339  ucnima  23341  ucnprima  23342  blcls  23568  prdsxmslem2  23591  isngp2  23659  tgioo  23865  xrtgioo  23875  xrsmopn  23881  opnreen  23900  cnheiborlem  24023  cnllycmp  24025  tcphcph  24306  rrxmvallem  24473  uniioombllem4  24655  dyadmbllem  24668  opnmbllem  24670  mbfimaopnlem  24724  mbflimsup  24735  i1fadd  24764  i1fmul  24765  itg1addlem4  24768  itg1addlem4OLD  24769  i1fmulc  24773  limciun  24963  dvlip2  25064  c1lip3  25068  lhop  25085  dvfsumlem2  25096  dvfsumrlimge0  25099  dvfsumrlim2  25101  ulmval  25444  psercnlem2  25488  efopnlem2  25717  efopn  25718  umgrres1lem  27580  upgrres1  27583  nbgrssvwo2  27632  ubthlem1  29133  issh2  29472  mdsymlem1  30666  padct  30956  xrofsup  30992  fz2ssnn0  31008  zarclsint  31724  tpr2rico  31764  sibfinima  32206  fct2relem  32477  bnj906  32810  bnj1014  32841  bnj1286  32899  bnj1408  32916  bnj1450  32930  bnj1452  32932  bnj1498  32941  bnj1501  32947  lfuhgr  32979  cvmopnlem  33140  cvmfolem  33141  cvmliftlem6  33152  cvmliftlem8  33154  cvmliftlem13  33158  cvmliftlem15  33160  cvmlift2lem9  33173  cvmlift2lem11  33175  cvmlift2lem12  33176  mclsppslem  33445  naddcllem  33758  naddov2  33761  madebdayim  33997  filnetlem4  34497  dissneqlem  35438  pibt2  35515  lindsdom  35698  opnmbllem0  35740  cnambfre  35752  heibor1lem  35894  osumcllem1N  37897  osumcllem2N  37898  pexmidlem6N  37916  dochexmidlem6  39406  dochexmidlem7  39407  mapdrvallem3  39587  k0004ss2  41651  cpcolld  41765  dvsconst  41837  dvsid  41838  dvsef  41839  iunconnlem2  42444  uzssd2  42847  climinf  43037  climsuse  43039  climresmpt  43090  climleltrp  43107  stoweidlem28  43459  stoweidlem50  43481  stoweidlem52  43483  stoweidlem53  43484  stoweidlem54  43485  fourierdlem54  43591  fourierdlem80  43617  meaiininclem  43914  caratheodorylem2  43955  hspmbllem2  44055  mbfresmf  44162  smfmbfcex  44182  smflimlem2  44194  smflimsuplem2  44241  smflimsuplem3  44242  smflimsuplem5  44244  smflimsuplem6  44245  isomuspgrlem2c  45170  upgredgssspr  45193  setrec1  46283  setrecsres  46293  aacllem  46391