Theorem sseqtrrdi 3976

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2723  df-ss 3919

This theorem is referenced by:  3sstr4g  3988  abssdv  4019  disjxiun  5088  knatar  7291  iunpw  7704  fviunfun  7877  frrlem8  8223  frrlem10  8225  frrlem12  8227  frrlem14  8229  fprresex  8240  tfrlem9  8304  tfrlem9a  8305  tfrlem13  8309  tz7.44-2  8326  tz7.44-3  8327  tz7.49  8364  naddcllem  8591  naddov2  8594  naddasslem1  8609  naddasslem2  8610  marypha1lem  9317  ordtypelem2  9405  ixpiunwdom  9476  oemapvali  9574  tcss  9634  tcel  9635  pwwf  9697  rankpwi  9713  rankval3b  9716  cplem1  9779  dfac12lem2  10033  infmap2  10105  ackbij1b  10126  ttukeylem6  10402  fpwwe2lem10  10528  fpwwe2lem11  10529  fpwwe2lem12  10530  fpwwe2  10531  uznnssnn  12790  pfxccatpfx2  14641  shftfval  14974  rexuzre  15257  climsup  15574  clim2prod  15792  fprodntriv  15846  eulerthlem2  16690  ramtlecl  16909  mreexexlem4d  17550  mreexdomd  17552  gsumpropd2lem  18584  gsumzaddlem  19831  gsum2d  19882  telgsums  19903  pgpfac1lem1  19986  pgpfac1lem3a  19988  pgpfac1lem3  19989  pgpfac1lem5  19991  lspsolvlem  21077  lbsextlem2  21094  dsmmacl  21676  eltopss  22820  difopn  22947  tgrest  23072  perfopn  23098  pnfnei  23133  mnfnei  23134  regsep2  23289  cncmp  23305  uncmp  23316  hauscmplem  23319  hauscmp  23320  conndisj  23329  cnconn  23335  conncompss  23346  2ndcctbss  23368  islly2  23397  comppfsc  23445  1stckgenlem  23466  txuni2  23478  ptbasfi  23494  ptpjopn  23525  txindis  23547  txtube  23553  hausdiag  23558  xkoinjcn  23600  tgqtop  23625  filconn  23796  elfm2  23861  flimclslem  23897  flffbas  23908  fclsbas  23934  flimfnfcls  23941  alexsubALT  23964  symgtgp  24019  ustssco  24128  isucn2  24191  ucnima  24193  ucnprima  24194  blcls  24419  prdsxmslem2  24442  isngp2  24510  tgioo  24709  xrtgioo  24720  xrsmopn  24726  opnreen  24745  cnheiborlem  24878  cnllycmp  24880  tcphcph  25162  rrxmvallem  25329  uniioombllem4  25512  dyadmbllem  25525  opnmbllem  25527  mbfimaopnlem  25581  mbflimsup  25592  i1fadd  25621  i1fmul  25622  itg1addlem4  25625  i1fmulc  25629  limciun  25820  dvlip2  25925  c1lip3  25929  lhop  25946  dvfsumlem2  25958  dvfsumlem2OLD  25959  dvfsumrlimge0  25962  dvfsumrlim2  25964  ulmval  26314  psercnlem2  26359  efopnlem2  26591  efopn  26592  madebdayim  27831  madefi  27856  oldfi  27857  addsbdaylem  27957  onsiso  28203  umgrres1lem  29286  upgrres1  29289  nbgrssvwo2  29338  ubthlem1  30845  issh2  31184  mdsymlem1  32378  iunxpssiun1  32543  padct  32696  xrofsup  32745  fz2ssnn0  32763  ccatws1f1o  32927  elrgspnlem1  33204  unitpidl1  33384  mxidlirred  33432  zarclsint  33880  tpr2rico  33920  sibfinima  34347  fct2relem  34605  bnj906  34937  bnj1014  34968  bnj1286  35026  bnj1408  35043  bnj1450  35057  bnj1452  35059  bnj1498  35068  bnj1501  35074  lfuhgr  35150  cvmopnlem  35310  cvmfolem  35311  cvmliftlem6  35322  cvmliftlem8  35324  cvmliftlem13  35328  cvmliftlem15  35330  cvmlift2lem9  35343  cvmlift2lem11  35345  cvmlift2lem12  35346  mclsppslem  35615  filnetlem4  36414  dissneqlem  37373  pibt2  37450  lindsdom  37653  opnmbllem0  37695  cnambfre  37707  heibor1lem  37848  osumcllem1N  39994  osumcllem2N  39995  pexmidlem6N  40013  dochexmidlem6  41503  dochexmidlem7  41504  mapdrvallem3  41684  evlsmhpvvval  42627  naddwordnexlem4  43433  k0004ss2  44184  cpcolld  44290  dvsconst  44362  dvsid  44363  dvsef  44364  iunconnlem2  44966  uzssd2  45454  climinf  45645  climsuse  45647  climresmpt  45696  climleltrp  45713  stoweidlem28  46065  stoweidlem50  46087  stoweidlem52  46089  stoweidlem53  46090  stoweidlem54  46091  fourierdlem54  46197  fourierdlem80  46223  meaiininclem  46523  caratheodorylem2  46564  hspmbllem2  46664  mbfresmf  46776  smfmbfcex  46797  smflimlem2  46809  smflimsuplem2  46858  smflimsuplem3  46859  smflimsuplem5  46861  smflimsuplem6  46862  gpgedgvtx1lem  47361  isuspgrim0  47924  gpgusgralem  48086  upgredgssspr  48173  setrec1  49722  setrecsres  49733  aacllem  49832