Theorem sseqtrrdi 3975

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3902

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2754  df-ss 3919

This theorem is used by:  3sstr4g  3987  abssdv  4018  disjxiun  5104  knatar  7364  iunpw  7774  fviunfun  7946  frrlem8  8296  frrlem10  8298  frrlem12  8300  frrlem14  8302  fprresex  8313  tfrlem9  8378  tfrlem9a  8379  tfrlem13  8383  tz7.44-2  8400  tz7.44-3  8401  tz7.49  8438  naddcllem  8668  naddov2  8671  naddasslem1  8687  naddasslem2  8688  marypha1lem  9407  ordtypelem2  9495  ixpiunwdom  9566  oemapvali  9667  tcss  9725  tcel  9726  pwwf  9793  rankpwi  9809  rankval3b  9812  cplem1  9893  cplem1OLD  9894  dfac12lem2  10151  infmap2  10223  ackbij1b  10244  ttukeylem6  10520  fpwwe2lem10  10653  fpwwe2lem11  10654  fpwwe2lem12  10655  fpwwe2  10656  uznnssnn  12948  pfxccatpfx2  14810  shftfval  15147  rexuzre  15444  climsup  15761  clim2prod  15981  fprodntriv  16035  eulerthlem2  16879  ramtlecl  17098  mreexexlem4d  17741  mreexdomd  17743  gsumpropd2lem  18787  gsumzaddlem  20054  gsum2d  20105  telgsums  20126  pgpfac1lem1  20209  pgpfac1lem3a  20211  pgpfac1lem3  20212  pgpfac1lem5  20214  lspsolvlem  21335  lbsextlem2  21352  dsmmacl  21960  lindsdom  22069  eltopss  23138  difopn  23265  tgrest  23390  perfopn  23416  pnfnei  23451  mnfnei  23452  regsep2  23607  cncmp  23623  uncmp  23634  hauscmplem  23637  hauscmp  23638  conndisj  23647  cnconn  23653  conncompss  23664  2ndcctbss  23687  islly2  23716  comppfsc  23764  1stckgenlem  23785  txuni2  23797  ptbasfi  23813  ptpjopn  23844  txindis  23866  txtube  23872  hausdiag  23877  xkoinjcn  23919  tgqtop  23944  filconn  24115  elfm2  24180  flimclslem  24216  flffbas  24227  fclsbas  24253  flimfnfcls  24260  alexsubALT  24283  symgtgp  24338  ustssco  24447  isucn2  24510  ucnima  24512  ucnprima  24513  blcls  24738  prdsxmslem2  24761  isngp2  24829  tgioo  25028  xrtgioo  25039  xrsmopn  25045  opnreen  25064  cnheiborlem  25188  cnllycmp  25190  tcphcph  25471  rrxmvallem  25638  uniioombllem4  25820  dyadmbllem  25833  opnmbllem  25835  mbfimaopnlem  25889  mbflimsup  25900  i1fadd  25929  i1fmul  25930  itg1addlem4  25933  i1fmulc  25937  limciun  26128  dvlip2  26229  c1lip3  26233  lhop  26250  dvfsumlem2  26261  dvfsumrlimge0  26264  dvfsumrlim2  26266  ulmval  26623  psercnlem2  26667  efopnlem2  26902  efopn  26903  madebdayim  28161  madefi  28186  oldfi  28187  addbdaylem  28290  oniso  28544  oldfib  28650  lfuhgr  29613  umgrres1lem  29778  upgrres1  29781  nbgrssvwo2  29830  ubthlem1  31359  issh2  31698  mdsymlem1  32892  iunxpssiun1  33049  padct  33197  xrofsup  33246  fz2ssnn0  33264  ccatws1f1o  33401  elrgspnlem1  33690  unitpidl1  33860  mxidlirred  33883  zarclsint  34390  tpr2rico  34430  sibfinima  34858  fct2relem  35113  bnj906  35447  bnj1014  35478  bnj1286  35536  bnj1408  35553  bnj1450  35567  bnj1452  35569  bnj1498  35578  bnj1501  35584  vonf1oonfo  35720  cvmopnlem  35865  cvmfolem  35866  cvmliftlem6  35877  cvmliftlem8  35879  cvmliftlem13  35883  cvmliftlem15  35885  cvmlift2lem9  35898  cvmlift2lem11  35900  cvmlift2lem12  35901  mclsppslem  36170  filnetlem4  37008  dissneqlem  38102  pibt2  38179  opnmbllem0  38413  cnambfre  38425  heibor1lem  38567  osumcllem1N  40837  osumcllem2N  40838  pexmidlem6N  40856  dochexmidlem6  42346  dochexmidlem7  42347  mapdrvallem3  42527  evlsmhpvvval  43449  naddwordnexlem4  44250  k0004ss2  45000  cpcolld  45090  dvsconst  45162  dvsid  45163  dvsef  45164  iunconnlem2  45765  uzssd2  46253  climinf  46444  climsuse  46446  climresmpt  46495  climleltrp  46512  stoweidlem28  46864  stoweidlem50  46886  stoweidlem52  46888  stoweidlem53  46889  stoweidlem54  46890  fourierdlem54  46996  fourierdlem80  47022  meaiininclem  47322  caratheodorylem2  47363  hspmbllem2  47463  mbfresmf  47575  smfmbfcex  47596  smflimlem2  47608  smflimsuplem2  47657  smflimsuplem3  47658  smflimsuplem5  47660  smflimsuplem6  47661  gpgedgvtx1lem  48231  isuspgrim0  48818  gpgusgralem  48980  upgredgssspr  49067  setrec1  50625  setrecsres  50636  aacllem  50780