Theorem sseqtrrdi 3979

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  3sstr4g  3991  abssdv  4022  disjxiun  5107  knatar  7357  iunpw  7771  fviunfun  7943  frrlem8  8291  frrlem10  8293  frrlem12  8295  frrlem14  8297  fprresex  8308  tfrlem9  8373  tfrlem9a  8374  tfrlem13  8378  tz7.44-2  8395  tz7.44-3  8396  tz7.49  8433  naddcllem  8663  naddov2  8666  naddasslem1  8682  naddasslem2  8683  marypha1lem  9394  ordtypelem2  9482  ixpiunwdom  9553  oemapvali  9654  tcss  9712  tcel  9713  pwwf  9780  rankpwi  9796  rankval3b  9799  cplem1  9876  dfac12lem2  10129  infmap2  10201  ackbij1b  10222  ttukeylem6  10499  fpwwe2lem10  10626  fpwwe2lem11  10627  fpwwe2lem12  10628  fpwwe2  10629  uznnssnn  12920  pfxccatpfx2  14776  shftfval  15109  rexuzre  15406  climsup  15723  clim2prod  15944  fprodntriv  15998  eulerthlem2  16842  ramtlecl  17061  mreexexlem4d  17704  mreexdomd  17706  gsumpropd2lem  18738  gsumzaddlem  19992  gsum2d  20043  telgsums  20064  pgpfac1lem1  20147  pgpfac1lem3a  20149  pgpfac1lem3  20150  pgpfac1lem5  20152  lspsolvlem  21247  lbsextlem2  21264  dsmmacl  21872  eltopss  23045  difopn  23172  tgrest  23297  perfopn  23323  pnfnei  23358  mnfnei  23359  regsep2  23514  cncmp  23530  uncmp  23541  hauscmplem  23544  hauscmp  23545  conndisj  23554  cnconn  23560  conncompss  23571  2ndcctbss  23593  islly2  23622  comppfsc  23670  1stckgenlem  23691  txuni2  23703  ptbasfi  23719  ptpjopn  23750  txindis  23772  txtube  23778  hausdiag  23783  xkoinjcn  23825  tgqtop  23850  filconn  24021  elfm2  24086  flimclslem  24122  flffbas  24133  fclsbas  24159  flimfnfcls  24166  alexsubALT  24189  symgtgp  24244  ustssco  24353  isucn2  24416  ucnima  24418  ucnprima  24419  blcls  24644  prdsxmslem2  24667  isngp2  24735  tgioo  24934  xrtgioo  24945  xrsmopn  24951  opnreen  24970  cnheiborlem  25094  cnllycmp  25096  tcphcph  25377  rrxmvallem  25544  uniioombllem4  25726  dyadmbllem  25739  opnmbllem  25741  mbfimaopnlem  25795  mbflimsup  25806  i1fadd  25835  i1fmul  25836  itg1addlem4  25839  i1fmulc  25843  limciun  26034  dvlip2  26135  c1lip3  26139  lhop  26156  dvfsumlem2  26167  dvfsumrlimge0  26170  dvfsumrlim2  26172  ulmval  26521  psercnlem2  26565  efopnlem2  26800  efopn  26801  madebdayim  28059  madefi  28084  oldfi  28085  addbdaylem  28188  oniso  28442  oldfib  28548  umgrres1lem  29638  upgrres1  29641  nbgrssvwo2  29690  ubthlem1  31200  issh2  31539  mdsymlem1  32733  iunxpssiun1  32891  padct  33041  xrofsup  33090  fz2ssnn0  33108  ccatws1f1o  33249  elrgspnlem1  33540  unitpidl1  33710  mxidlirred  33733  zarclsint  34240  tpr2rico  34280  sibfinima  34707  fct2relem  34962  bnj906  35296  bnj1014  35327  bnj1286  35385  bnj1408  35402  bnj1450  35416  bnj1452  35418  bnj1498  35427  bnj1501  35433  vonf1oonfo  35577  lfuhgr  35588  cvmopnlem  35748  cvmfolem  35749  cvmliftlem6  35760  cvmliftlem8  35762  cvmliftlem13  35766  cvmliftlem15  35768  cvmlift2lem9  35781  cvmlift2lem11  35783  cvmlift2lem12  35784  mclsppslem  36053  filnetlem4  36870  dissneqlem  37964  pibt2  38041  lindsdom  38243  opnmbllem0  38285  cnambfre  38297  heibor1lem  38438  osumcllem1N  40708  osumcllem2N  40709  pexmidlem6N  40727  dochexmidlem6  42217  dochexmidlem7  42218  mapdrvallem3  42398  evlsmhpvvval  43307  naddwordnexlem4  44108  k0004ss2  44858  cpcolld  44948  dvsconst  45020  dvsid  45021  dvsef  45022  iunconnlem2  45623  uzssd2  46111  climinf  46302  climsuse  46304  climresmpt  46353  climleltrp  46370  stoweidlem28  46722  stoweidlem50  46744  stoweidlem52  46746  stoweidlem53  46747  stoweidlem54  46748  fourierdlem54  46854  fourierdlem80  46880  meaiininclem  47180  caratheodorylem2  47221  hspmbllem2  47321  mbfresmf  47433  smfmbfcex  47454  smflimlem2  47466  smflimsuplem2  47515  smflimsuplem3  47516  smflimsuplem5  47518  smflimsuplem6  47519  gpgedgvtx1lem  48049  isuspgrim0  48636  gpgusgralem  48798  upgredgssspr  48885  setrec1  50446  setrecsres  50457  aacllem  50578