Theorem sseqtrrdi 4033

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1536  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-v 3475  df-in 3956  df-ss 3966

This theorem is referenced by:  abssdv  4065  disjxiun  5149  knatar  7371  iunpw  7779  fviunfun  7954  frrlem8  8305  frrlem10  8307  frrlem12  8309  frrlem14  8311  fprresex  8322  wfrdmclOLD  8344  wfrlem12OLD  8347  wfrlem16OLD  8351  wfrlem17OLD  8352  tfrlem9  8412  tfrlem9a  8413  tfrlem13  8417  tz7.44-2  8434  tz7.44-3  8435  tz7.49  8472  naddcllem  8703  naddov2  8706  naddasslem1  8721  naddasslem2  8722  marypha1lem  9464  ordtypelem2  9550  ixpiunwdom  9621  oemapvali  9715  tcss  9775  tcel  9776  pwwf  9838  rankpwi  9854  rankval3b  9857  cplem1  9920  dfac12lem2  10175  infmap2  10249  ackbij1b  10270  ttukeylem6  10545  fpwwe2lem10  10671  fpwwe2lem11  10672  fpwwe2lem12  10673  fpwwe2  10674  uznnssnn  12917  pfxccatpfx2  14727  shftfval  15057  rexuzre  15339  climsup  15656  clim2prod  15874  fprodntriv  15926  eulerthlem2  16758  ramtlecl  16976  mreexexlem4d  17634  mreexdomd  17636  gsumpropd2lem  18646  gsumzaddlem  19883  gsum2d  19934  telgsums  19955  pgpfac1lem1  20038  pgpfac1lem3a  20040  pgpfac1lem3  20041  pgpfac1lem5  20043  lspsolvlem  21037  lbsextlem2  21054  dsmmacl  21682  eltopss  22829  difopn  22958  tgrest  23083  perfopn  23109  pnfnei  23144  mnfnei  23145  regsep2  23300  cncmp  23316  uncmp  23327  hauscmplem  23330  hauscmp  23331  conndisj  23340  cnconn  23346  conncompss  23357  2ndcctbss  23379  islly2  23408  comppfsc  23456  1stckgenlem  23477  txuni2  23489  ptbasfi  23505  ptpjopn  23536  txindis  23558  txtube  23564  hausdiag  23569  xkoinjcn  23611  tgqtop  23636  filconn  23807  elfm2  23872  flimclslem  23908  flffbas  23919  fclsbas  23945  flimfnfcls  23952  alexsubALT  23975  symgtgp  24030  ustssco  24139  isucn2  24204  ucnima  24206  ucnprima  24207  blcls  24435  prdsxmslem2  24458  isngp2  24526  tgioo  24732  xrtgioo  24742  xrsmopn  24748  opnreen  24767  cnheiborlem  24900  cnllycmp  24902  tcphcph  25185  rrxmvallem  25352  uniioombllem4  25535  dyadmbllem  25548  opnmbllem  25550  mbfimaopnlem  25604  mbflimsup  25615  i1fadd  25644  i1fmul  25645  itg1addlem4  25648  itg1addlem4OLD  25649  i1fmulc  25653  limciun  25843  dvlip2  25948  c1lip3  25952  lhop  25969  dvfsumlem2  25981  dvfsumlem2OLD  25982  dvfsumrlimge0  25985  dvfsumrlim2  25987  ulmval  26336  psercnlem2  26381  efopnlem2  26611  efopn  26612  madebdayim  27834  umgrres1lem  29143  upgrres1  29146  nbgrssvwo2  29195  ubthlem1  30700  issh2  31039  mdsymlem1  32233  padct  32522  xrofsup  32558  fz2ssnn0  32574  unitpidl1  33164  mxidlirred  33210  zarclsint  33506  tpr2rico  33546  sibfinima  33992  fct2relem  34262  bnj906  34594  bnj1014  34625  bnj1286  34683  bnj1408  34700  bnj1450  34714  bnj1452  34716  bnj1498  34725  bnj1501  34731  lfuhgr  34760  cvmopnlem  34921  cvmfolem  34922  cvmliftlem6  34933  cvmliftlem8  34935  cvmliftlem13  34939  cvmliftlem15  34941  cvmlift2lem9  34954  cvmlift2lem11  34956  cvmlift2lem12  34957  mclsppslem  35226  filnetlem4  35898  dissneqlem  36852  pibt2  36929  lindsdom  37120  opnmbllem0  37162  cnambfre  37174  heibor1lem  37315  osumcllem1N  39461  osumcllem2N  39462  pexmidlem6N  39480  dochexmidlem6  40970  dochexmidlem7  40971  mapdrvallem3  41151  evlsmhpvvval  41859  naddwordnexlem4  42862  k0004ss2  43613  cpcolld  43726  dvsconst  43798  dvsid  43799  dvsef  43800  iunconnlem2  44405  uzssd2  44828  climinf  45023  climsuse  45025  climresmpt  45076  climleltrp  45093  stoweidlem28  45445  stoweidlem50  45467  stoweidlem52  45469  stoweidlem53  45470  stoweidlem54  45471  fourierdlem54  45577  fourierdlem80  45603  meaiininclem  45903  caratheodorylem2  45944  hspmbllem2  46044  mbfresmf  46156  smfmbfcex  46177  smflimlem2  46189  smflimsuplem2  46238  smflimsuplem3  46239  smflimsuplem5  46241  smflimsuplem6  46242  isuspgrim0  47248  upgredgssspr  47283  setrec1  48200  setrecsres  48211  aacllem  48312