Theorem sseqtrrdi 4025

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 4024	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  3sstr4g  4037  abssdv  4068  disjxiun  5140  knatar  7377  iunpw  7791  fviunfun  7969  frrlem8  8318  frrlem10  8320  frrlem12  8322  frrlem14  8324  fprresex  8335  wfrdmclOLD  8357  wfrlem12OLD  8360  wfrlem16OLD  8364  wfrlem17OLD  8365  tfrlem9  8425  tfrlem9a  8426  tfrlem13  8430  tz7.44-2  8447  tz7.44-3  8448  tz7.49  8485  naddcllem  8714  naddov2  8717  naddasslem1  8732  naddasslem2  8733  marypha1lem  9473  ordtypelem2  9559  ixpiunwdom  9630  oemapvali  9724  tcss  9784  tcel  9785  pwwf  9847  rankpwi  9863  rankval3b  9866  cplem1  9929  dfac12lem2  10185  infmap2  10257  ackbij1b  10278  ttukeylem6  10554  fpwwe2lem10  10680  fpwwe2lem11  10681  fpwwe2lem12  10682  fpwwe2  10683  uznnssnn  12937  pfxccatpfx2  14775  shftfval  15109  rexuzre  15391  climsup  15706  clim2prod  15924  fprodntriv  15978  eulerthlem2  16819  ramtlecl  17038  mreexexlem4d  17690  mreexdomd  17692  gsumpropd2lem  18692  gsumzaddlem  19939  gsum2d  19990  telgsums  20011  pgpfac1lem1  20094  pgpfac1lem3a  20096  pgpfac1lem3  20097  pgpfac1lem5  20099  lspsolvlem  21144  lbsextlem2  21161  dsmmacl  21761  eltopss  22913  difopn  23042  tgrest  23167  perfopn  23193  pnfnei  23228  mnfnei  23229  regsep2  23384  cncmp  23400  uncmp  23411  hauscmplem  23414  hauscmp  23415  conndisj  23424  cnconn  23430  conncompss  23441  2ndcctbss  23463  islly2  23492  comppfsc  23540  1stckgenlem  23561  txuni2  23573  ptbasfi  23589  ptpjopn  23620  txindis  23642  txtube  23648  hausdiag  23653  xkoinjcn  23695  tgqtop  23720  filconn  23891  elfm2  23956  flimclslem  23992  flffbas  24003  fclsbas  24029  flimfnfcls  24036  alexsubALT  24059  symgtgp  24114  ustssco  24223  isucn2  24288  ucnima  24290  ucnprima  24291  blcls  24519  prdsxmslem2  24542  isngp2  24610  tgioo  24817  xrtgioo  24828  xrsmopn  24834  opnreen  24853  cnheiborlem  24986  cnllycmp  24988  tcphcph  25271  rrxmvallem  25438  uniioombllem4  25621  dyadmbllem  25634  opnmbllem  25636  mbfimaopnlem  25690  mbflimsup  25701  i1fadd  25730  i1fmul  25731  itg1addlem4  25734  i1fmulc  25738  limciun  25929  dvlip2  26034  c1lip3  26038  lhop  26055  dvfsumlem2  26067  dvfsumlem2OLD  26068  dvfsumrlimge0  26071  dvfsumrlim2  26073  ulmval  26423  psercnlem2  26468  efopnlem2  26699  efopn  26700  madebdayim  27926  madefi  27950  oldfi  27951  addsbdaylem  28049  umgrres1lem  29327  upgrres1  29330  nbgrssvwo2  29379  ubthlem1  30889  issh2  31228  mdsymlem1  32422  iunxpssiun1  32581  padct  32731  xrofsup  32771  fz2ssnn0  32787  ccatws1f1o  32936  elrgspnlem1  33246  unitpidl1  33452  mxidlirred  33500  zarclsint  33871  tpr2rico  33911  sibfinima  34341  fct2relem  34612  bnj906  34944  bnj1014  34975  bnj1286  35033  bnj1408  35050  bnj1450  35064  bnj1452  35066  bnj1498  35075  bnj1501  35081  lfuhgr  35123  cvmopnlem  35283  cvmfolem  35284  cvmliftlem6  35295  cvmliftlem8  35297  cvmliftlem13  35301  cvmliftlem15  35303  cvmlift2lem9  35316  cvmlift2lem11  35318  cvmlift2lem12  35319  mclsppslem  35588  filnetlem4  36382  dissneqlem  37341  pibt2  37418  lindsdom  37621  opnmbllem0  37663  cnambfre  37675  heibor1lem  37816  osumcllem1N  39958  osumcllem2N  39959  pexmidlem6N  39977  dochexmidlem6  41467  dochexmidlem7  41468  mapdrvallem3  41648  evlsmhpvvval  42605  naddwordnexlem4  43414  k0004ss2  44165  cpcolld  44277  dvsconst  44349  dvsid  44350  dvsef  44351  iunconnlem2  44955  uzssd2  45428  climinf  45621  climsuse  45623  climresmpt  45674  climleltrp  45691  stoweidlem28  46043  stoweidlem50  46065  stoweidlem52  46067  stoweidlem53  46068  stoweidlem54  46069  fourierdlem54  46175  fourierdlem80  46201  meaiininclem  46501  caratheodorylem2  46542  hspmbllem2  46642  mbfresmf  46754  smfmbfcex  46775  smflimlem2  46787  smflimsuplem2  46836  smflimsuplem3  46837  smflimsuplem5  46839  smflimsuplem6  46840  isuspgrim0  47872  gpgusgralem  48011  gpgedgvtx1lem  48017  upgredgssspr  48059  setrec1  49210  setrecsres  49221  aacllem  49320