Theorem sseqtrrdi 4034

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  abssdv  4066  disjxiun  5146  knatar  7354  iunpw  7758  fviunfun  7931  frrlem8  8278  frrlem10  8280  frrlem12  8282  frrlem14  8284  fprresex  8295  wfrdmclOLD  8317  wfrlem12OLD  8320  wfrlem16OLD  8324  wfrlem17OLD  8325  tfrlem9  8385  tfrlem9a  8386  tfrlem13  8390  tz7.44-2  8407  tz7.44-3  8408  tz7.49  8445  naddcllem  8675  naddov2  8678  naddasslem1  8693  naddasslem2  8694  marypha1lem  9428  ordtypelem2  9514  ixpiunwdom  9585  oemapvali  9679  tcss  9739  tcel  9740  pwwf  9802  rankpwi  9818  rankval3b  9821  cplem1  9884  dfac12lem2  10139  infmap2  10213  ackbij1b  10234  ttukeylem6  10509  fpwwe2lem10  10635  fpwwe2lem11  10636  fpwwe2lem12  10637  fpwwe2  10638  uznnssnn  12879  pfxccatpfx2  14687  shftfval  15017  rexuzre  15299  climsup  15616  clim2prod  15834  fprodntriv  15886  eulerthlem2  16715  ramtlecl  16933  mreexexlem4d  17591  mreexdomd  17593  gsumpropd2lem  18598  gsumzaddlem  19789  gsum2d  19840  telgsums  19861  pgpfac1lem1  19944  pgpfac1lem3a  19946  pgpfac1lem3  19947  pgpfac1lem5  19949  lspsolvlem  20755  lbsextlem2  20772  dsmmacl  21296  eltopss  22409  difopn  22538  tgrest  22663  perfopn  22689  pnfnei  22724  mnfnei  22725  regsep2  22880  cncmp  22896  uncmp  22907  hauscmplem  22910  hauscmp  22911  conndisj  22920  cnconn  22926  conncompss  22937  2ndcctbss  22959  islly2  22988  comppfsc  23036  1stckgenlem  23057  txuni2  23069  ptbasfi  23085  ptpjopn  23116  txindis  23138  txtube  23144  hausdiag  23149  xkoinjcn  23191  tgqtop  23216  filconn  23387  elfm2  23452  flimclslem  23488  flffbas  23499  fclsbas  23525  flimfnfcls  23532  alexsubALT  23555  symgtgp  23610  ustssco  23719  isucn2  23784  ucnima  23786  ucnprima  23787  blcls  24015  prdsxmslem2  24038  isngp2  24106  tgioo  24312  xrtgioo  24322  xrsmopn  24328  opnreen  24347  cnheiborlem  24470  cnllycmp  24472  tcphcph  24754  rrxmvallem  24921  uniioombllem4  25103  dyadmbllem  25116  opnmbllem  25118  mbfimaopnlem  25172  mbflimsup  25183  i1fadd  25212  i1fmul  25213  itg1addlem4  25216  itg1addlem4OLD  25217  i1fmulc  25221  limciun  25411  dvlip2  25512  c1lip3  25516  lhop  25533  dvfsumlem2  25544  dvfsumrlimge0  25547  dvfsumrlim2  25549  ulmval  25892  psercnlem2  25936  efopnlem2  26165  efopn  26166  madebdayim  27382  umgrres1lem  28567  upgrres1  28570  nbgrssvwo2  28619  ubthlem1  30123  issh2  30462  mdsymlem1  31656  padct  31944  xrofsup  31980  fz2ssnn0  31996  unitpidl1  32542  mxidlirred  32588  zarclsint  32852  tpr2rico  32892  sibfinima  33338  fct2relem  33609  bnj906  33941  bnj1014  33972  bnj1286  34030  bnj1408  34047  bnj1450  34061  bnj1452  34063  bnj1498  34072  bnj1501  34078  lfuhgr  34108  cvmopnlem  34269  cvmfolem  34270  cvmliftlem6  34281  cvmliftlem8  34283  cvmliftlem13  34287  cvmliftlem15  34289  cvmlift2lem9  34302  cvmlift2lem11  34304  cvmlift2lem12  34305  mclsppslem  34574  gg-dvfsumlem2  35183  filnetlem4  35266  dissneqlem  36221  pibt2  36298  lindsdom  36482  opnmbllem0  36524  cnambfre  36536  heibor1lem  36677  osumcllem1N  38827  osumcllem2N  38828  pexmidlem6N  38846  dochexmidlem6  40336  dochexmidlem7  40337  mapdrvallem3  40517  evlsmhpvvval  41167  naddwordnexlem4  42152  k0004ss2  42903  cpcolld  43017  dvsconst  43089  dvsid  43090  dvsef  43091  iunconnlem2  43696  uzssd2  44127  climinf  44322  climsuse  44324  climresmpt  44375  climleltrp  44392  stoweidlem28  44744  stoweidlem50  44766  stoweidlem52  44768  stoweidlem53  44769  stoweidlem54  44770  fourierdlem54  44876  fourierdlem80  44902  meaiininclem  45202  caratheodorylem2  45243  hspmbllem2  45343  mbfresmf  45455  smfmbfcex  45476  smflimlem2  45488  smflimsuplem2  45537  smflimsuplem3  45538  smflimsuplem5  45540  smflimsuplem6  45541  isomuspgrlem2c  46498  upgredgssspr  46521  setrec1  47736  setrecsres  47747  aacllem  47848