Theorem sseqtrrdi 4000

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3926

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2727  df-ss 3943

This theorem is referenced by:  3sstr4g  4012  abssdv  4043  disjxiun  5116  knatar  7350  iunpw  7765  fviunfun  7943  frrlem8  8292  frrlem10  8294  frrlem12  8296  frrlem14  8298  fprresex  8309  wfrdmclOLD  8331  wfrlem12OLD  8334  wfrlem16OLD  8338  wfrlem17OLD  8339  tfrlem9  8399  tfrlem9a  8400  tfrlem13  8404  tz7.44-2  8421  tz7.44-3  8422  tz7.49  8459  naddcllem  8688  naddov2  8691  naddasslem1  8706  naddasslem2  8707  marypha1lem  9445  ordtypelem2  9533  ixpiunwdom  9604  oemapvali  9698  tcss  9758  tcel  9759  pwwf  9821  rankpwi  9837  rankval3b  9840  cplem1  9903  dfac12lem2  10159  infmap2  10231  ackbij1b  10252  ttukeylem6  10528  fpwwe2lem10  10654  fpwwe2lem11  10655  fpwwe2lem12  10656  fpwwe2  10657  uznnssnn  12911  pfxccatpfx2  14755  shftfval  15089  rexuzre  15371  climsup  15686  clim2prod  15904  fprodntriv  15958  eulerthlem2  16801  ramtlecl  17020  mreexexlem4d  17659  mreexdomd  17661  gsumpropd2lem  18657  gsumzaddlem  19902  gsum2d  19953  telgsums  19974  pgpfac1lem1  20057  pgpfac1lem3a  20059  pgpfac1lem3  20060  pgpfac1lem5  20062  lspsolvlem  21103  lbsextlem2  21120  dsmmacl  21701  eltopss  22845  difopn  22972  tgrest  23097  perfopn  23123  pnfnei  23158  mnfnei  23159  regsep2  23314  cncmp  23330  uncmp  23341  hauscmplem  23344  hauscmp  23345  conndisj  23354  cnconn  23360  conncompss  23371  2ndcctbss  23393  islly2  23422  comppfsc  23470  1stckgenlem  23491  txuni2  23503  ptbasfi  23519  ptpjopn  23550  txindis  23572  txtube  23578  hausdiag  23583  xkoinjcn  23625  tgqtop  23650  filconn  23821  elfm2  23886  flimclslem  23922  flffbas  23933  fclsbas  23959  flimfnfcls  23966  alexsubALT  23989  symgtgp  24044  ustssco  24153  isucn2  24217  ucnima  24219  ucnprima  24220  blcls  24445  prdsxmslem2  24468  isngp2  24536  tgioo  24735  xrtgioo  24746  xrsmopn  24752  opnreen  24771  cnheiborlem  24904  cnllycmp  24906  tcphcph  25189  rrxmvallem  25356  uniioombllem4  25539  dyadmbllem  25552  opnmbllem  25554  mbfimaopnlem  25608  mbflimsup  25619  i1fadd  25648  i1fmul  25649  itg1addlem4  25652  i1fmulc  25656  limciun  25847  dvlip2  25952  c1lip3  25956  lhop  25973  dvfsumlem2  25985  dvfsumlem2OLD  25986  dvfsumrlimge0  25989  dvfsumrlim2  25991  ulmval  26341  psercnlem2  26386  efopnlem2  26618  efopn  26619  madebdayim  27851  madefi  27876  oldfi  27877  addsbdaylem  27975  onsiso  28221  umgrres1lem  29289  upgrres1  29292  nbgrssvwo2  29341  ubthlem1  30851  issh2  31190  mdsymlem1  32384  iunxpssiun1  32549  padct  32697  xrofsup  32744  fz2ssnn0  32762  ccatws1f1o  32927  elrgspnlem1  33237  unitpidl1  33439  mxidlirred  33487  zarclsint  33903  tpr2rico  33943  sibfinima  34371  fct2relem  34629  bnj906  34961  bnj1014  34992  bnj1286  35050  bnj1408  35067  bnj1450  35081  bnj1452  35083  bnj1498  35092  bnj1501  35098  lfuhgr  35140  cvmopnlem  35300  cvmfolem  35301  cvmliftlem6  35312  cvmliftlem8  35314  cvmliftlem13  35318  cvmliftlem15  35320  cvmlift2lem9  35333  cvmlift2lem11  35335  cvmlift2lem12  35336  mclsppslem  35605  filnetlem4  36399  dissneqlem  37358  pibt2  37435  lindsdom  37638  opnmbllem0  37680  cnambfre  37692  heibor1lem  37833  osumcllem1N  39975  osumcllem2N  39976  pexmidlem6N  39994  dochexmidlem6  41484  dochexmidlem7  41485  mapdrvallem3  41665  evlsmhpvvval  42618  naddwordnexlem4  43425  k0004ss2  44176  cpcolld  44282  dvsconst  44354  dvsid  44355  dvsef  44356  iunconnlem2  44959  uzssd2  45444  climinf  45635  climsuse  45637  climresmpt  45688  climleltrp  45705  stoweidlem28  46057  stoweidlem50  46079  stoweidlem52  46081  stoweidlem53  46082  stoweidlem54  46083  fourierdlem54  46189  fourierdlem80  46215  meaiininclem  46515  caratheodorylem2  46556  hspmbllem2  46656  mbfresmf  46768  smfmbfcex  46789  smflimlem2  46801  smflimsuplem2  46850  smflimsuplem3  46851  smflimsuplem5  46853  smflimsuplem6  46854  gpgedgvtx1lem  47360  isuspgrim0  47907  gpgusgralem  48060  upgredgssspr  48118  setrec1  49555  setrecsres  49566  aacllem  49665