Theorem sseqtrrdi 4046

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

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  abssdv  4077  disjxiun  5144  knatar  7376  iunpw  7789  fviunfun  7967  frrlem8  8316  frrlem10  8318  frrlem12  8320  frrlem14  8322  fprresex  8333  wfrdmclOLD  8355  wfrlem12OLD  8358  wfrlem16OLD  8362  wfrlem17OLD  8363  tfrlem9  8423  tfrlem9a  8424  tfrlem13  8428  tz7.44-2  8445  tz7.44-3  8446  tz7.49  8483  naddcllem  8712  naddov2  8715  naddasslem1  8730  naddasslem2  8731  marypha1lem  9470  ordtypelem2  9556  ixpiunwdom  9627  oemapvali  9721  tcss  9781  tcel  9782  pwwf  9844  rankpwi  9860  rankval3b  9863  cplem1  9926  dfac12lem2  10182  infmap2  10254  ackbij1b  10275  ttukeylem6  10551  fpwwe2lem10  10677  fpwwe2lem11  10678  fpwwe2lem12  10679  fpwwe2  10680  uznnssnn  12934  pfxccatpfx2  14771  shftfval  15105  rexuzre  15387  climsup  15702  clim2prod  15920  fprodntriv  15974  eulerthlem2  16815  ramtlecl  17033  mreexexlem4d  17691  mreexdomd  17693  gsumpropd2lem  18704  gsumzaddlem  19953  gsum2d  20004  telgsums  20025  pgpfac1lem1  20108  pgpfac1lem3a  20110  pgpfac1lem3  20111  pgpfac1lem5  20113  lspsolvlem  21161  lbsextlem2  21178  dsmmacl  21778  eltopss  22928  difopn  23057  tgrest  23182  perfopn  23208  pnfnei  23243  mnfnei  23244  regsep2  23399  cncmp  23415  uncmp  23426  hauscmplem  23429  hauscmp  23430  conndisj  23439  cnconn  23445  conncompss  23456  2ndcctbss  23478  islly2  23507  comppfsc  23555  1stckgenlem  23576  txuni2  23588  ptbasfi  23604  ptpjopn  23635  txindis  23657  txtube  23663  hausdiag  23668  xkoinjcn  23710  tgqtop  23735  filconn  23906  elfm2  23971  flimclslem  24007  flffbas  24018  fclsbas  24044  flimfnfcls  24051  alexsubALT  24074  symgtgp  24129  ustssco  24238  isucn2  24303  ucnima  24305  ucnprima  24306  blcls  24534  prdsxmslem2  24557  isngp2  24625  tgioo  24831  xrtgioo  24841  xrsmopn  24847  opnreen  24866  cnheiborlem  24999  cnllycmp  25001  tcphcph  25284  rrxmvallem  25451  uniioombllem4  25634  dyadmbllem  25647  opnmbllem  25649  mbfimaopnlem  25703  mbflimsup  25714  i1fadd  25743  i1fmul  25744  itg1addlem4  25747  itg1addlem4OLD  25748  i1fmulc  25752  limciun  25943  dvlip2  26048  c1lip3  26052  lhop  26069  dvfsumlem2  26081  dvfsumlem2OLD  26082  dvfsumrlimge0  26085  dvfsumrlim2  26087  ulmval  26437  psercnlem2  26482  efopnlem2  26713  efopn  26714  madebdayim  27940  madefi  27964  oldfi  27965  addsbdaylem  28063  umgrres1lem  29341  upgrres1  29344  nbgrssvwo2  29393  ubthlem1  30898  issh2  31237  mdsymlem1  32431  padct  32736  xrofsup  32777  fz2ssnn0  32793  ccatws1f1o  32920  elrgspnlem1  33231  unitpidl1  33431  mxidlirred  33479  zarclsint  33832  tpr2rico  33872  sibfinima  34320  fct2relem  34590  bnj906  34922  bnj1014  34953  bnj1286  35011  bnj1408  35028  bnj1450  35042  bnj1452  35044  bnj1498  35053  bnj1501  35059  lfuhgr  35101  cvmopnlem  35262  cvmfolem  35263  cvmliftlem6  35274  cvmliftlem8  35276  cvmliftlem13  35280  cvmliftlem15  35282  cvmlift2lem9  35295  cvmlift2lem11  35297  cvmlift2lem12  35298  mclsppslem  35567  filnetlem4  36363  dissneqlem  37322  pibt2  37399  lindsdom  37600  opnmbllem0  37642  cnambfre  37654  heibor1lem  37795  osumcllem1N  39938  osumcllem2N  39939  pexmidlem6N  39957  dochexmidlem6  41447  dochexmidlem7  41448  mapdrvallem3  41628  evlsmhpvvval  42581  naddwordnexlem4  43390  k0004ss2  44141  cpcolld  44253  dvsconst  44325  dvsid  44326  dvsef  44327  iunconnlem2  44932  uzssd2  45366  climinf  45561  climsuse  45563  climresmpt  45614  climleltrp  45631  stoweidlem28  45983  stoweidlem50  46005  stoweidlem52  46007  stoweidlem53  46008  stoweidlem54  46009  fourierdlem54  46115  fourierdlem80  46141  meaiininclem  46441  caratheodorylem2  46482  hspmbllem2  46582  mbfresmf  46694  smfmbfcex  46715  smflimlem2  46727  smflimsuplem2  46776  smflimsuplem3  46777  smflimsuplem5  46779  smflimsuplem6  46780  isuspgrim0  47809  gpgusgralem  47945  gpgedgvtx1lem  47951  upgredgssspr  47986  setrec1  48921  setrecsres  48932  aacllem  49031