Theorem sseqtrrdi 3977

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1545  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-v 3433  df-in 3899  df-ss 3909

This theorem is referenced by:  disjxiun  5076  knatar  7225  iunpw  7616  fviunfun  7782  frrlem8  8101  frrlem10  8103  frrlem12  8105  frrlem14  8107  fprresex  8118  wfrdmclOLD  8140  wfrlem12OLD  8143  wfrlem16OLD  8147  wfrlem17OLD  8148  tfrlem9  8208  tfrlem9a  8209  tfrlem13  8213  tz7.44-2  8230  tz7.44-3  8231  tz7.49  8268  marypha1lem  9180  ordtypelem2  9266  ixpiunwdom  9337  oemapvali  9430  trpredpred  9485  trpredtr  9487  trpredrec  9494  tcss  9512  tcel  9513  pwwf  9576  rankpwi  9592  rankval3b  9595  cplem1  9658  dfac12lem2  9911  infmap2  9985  ackbij1b  10006  ttukeylem6  10281  fpwwe2lem10  10407  fpwwe2lem11  10408  fpwwe2lem12  10409  fpwwe2  10410  uznnssnn  12646  pfxccatpfx2  14461  shftfval  14792  rexuzre  15075  climsup  15392  clim2prod  15611  fprodntriv  15663  eulerthlem2  16494  ramtlecl  16712  mreexexlem4d  17367  mreexdomd  17369  gsumpropd2lem  18374  gsumzaddlem  19533  gsum2d  19584  telgsums  19605  pgpfac1lem1  19688  pgpfac1lem3a  19690  pgpfac1lem3  19691  pgpfac1lem5  19693  lspsolvlem  20415  lbsextlem2  20432  dsmmacl  20959  eltopss  22067  difopn  22196  tgrest  22321  perfopn  22347  pnfnei  22382  mnfnei  22383  regsep2  22538  cncmp  22554  uncmp  22565  hauscmplem  22568  hauscmp  22569  conndisj  22578  cnconn  22584  conncompss  22595  2ndcctbss  22617  islly2  22646  comppfsc  22694  1stckgenlem  22715  txuni2  22727  ptbasfi  22743  ptpjopn  22774  txindis  22796  txtube  22802  hausdiag  22807  xkoinjcn  22849  tgqtop  22874  filconn  23045  elfm2  23110  flimclslem  23146  flffbas  23157  fclsbas  23183  flimfnfcls  23190  alexsubALT  23213  symgtgp  23268  ustssco  23377  isucn2  23442  ucnima  23444  ucnprima  23445  blcls  23673  prdsxmslem2  23696  isngp2  23764  tgioo  23970  xrtgioo  23980  xrsmopn  23986  opnreen  24005  cnheiborlem  24128  cnllycmp  24130  tcphcph  24412  rrxmvallem  24579  uniioombllem4  24761  dyadmbllem  24774  opnmbllem  24776  mbfimaopnlem  24830  mbflimsup  24841  i1fadd  24870  i1fmul  24871  itg1addlem4  24874  itg1addlem4OLD  24875  i1fmulc  24879  limciun  25069  dvlip2  25170  c1lip3  25174  lhop  25191  dvfsumlem2  25202  dvfsumrlimge0  25205  dvfsumrlim2  25207  ulmval  25550  psercnlem2  25594  efopnlem2  25823  efopn  25824  umgrres1lem  27688  upgrres1  27691  nbgrssvwo2  27740  ubthlem1  29241  issh2  29580  mdsymlem1  30774  padct  31063  xrofsup  31099  fz2ssnn0  31115  zarclsint  31831  tpr2rico  31871  sibfinima  32315  fct2relem  32586  bnj906  32919  bnj1014  32950  bnj1286  33008  bnj1408  33025  bnj1450  33039  bnj1452  33041  bnj1498  33050  bnj1501  33056  lfuhgr  33088  cvmopnlem  33249  cvmfolem  33250  cvmliftlem6  33261  cvmliftlem8  33263  cvmliftlem13  33267  cvmliftlem15  33269  cvmlift2lem9  33282  cvmlift2lem11  33284  cvmlift2lem12  33285  mclsppslem  33554  naddcllem  33840  naddov2  33843  madebdayim  34079  filnetlem4  34579  dissneqlem  35520  pibt2  35597  lindsdom  35780  opnmbllem0  35822  cnambfre  35834  heibor1lem  35976  osumcllem1N  37979  osumcllem2N  37980  pexmidlem6N  37998  dochexmidlem6  39488  dochexmidlem7  39489  mapdrvallem3  39669  k0004ss2  41744  cpcolld  41858  dvsconst  41930  dvsid  41931  dvsef  41932  iunconnlem2  42537  uzssd2  42939  climinf  43129  climsuse  43131  climresmpt  43182  climleltrp  43199  stoweidlem28  43551  stoweidlem50  43573  stoweidlem52  43575  stoweidlem53  43576  stoweidlem54  43577  fourierdlem54  43683  fourierdlem80  43709  meaiininclem  44006  caratheodorylem2  44047  hspmbllem2  44147  mbfresmf  44254  smfmbfcex  44274  smflimlem2  44286  smflimsuplem2  44333  smflimsuplem3  44334  smflimsuplem5  44336  smflimsuplem6  44337  isomuspgrlem2c  45261  upgredgssspr  45284  setrec1  46376  setrecsres  46386  aacllem  46484