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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  3sstr4g  3989  abssdv  4021  disjxiun  5097  knatar  7313  iunpw  7726  fviunfun  7899  frrlem8  8245  frrlem10  8247  frrlem12  8249  frrlem14  8251  fprresex  8262  tfrlem9  8326  tfrlem9a  8327  tfrlem13  8331  tz7.44-2  8348  tz7.44-3  8349  tz7.49  8386  naddcllem  8614  naddov2  8617  naddasslem1  8632  naddasslem2  8633  marypha1lem  9348  ordtypelem2  9436  ixpiunwdom  9507  oemapvali  9605  tcss  9663  tcel  9664  pwwf  9731  rankpwi  9747  rankval3b  9750  cplem1  9813  dfac12lem2  10067  infmap2  10139  ackbij1b  10160  ttukeylem6  10436  fpwwe2lem10  10563  fpwwe2lem11  10564  fpwwe2lem12  10565  fpwwe2  10566  uznnssnn  12820  pfxccatpfx2  14672  shftfval  15005  rexuzre  15288  climsup  15605  clim2prod  15823  fprodntriv  15877  eulerthlem2  16721  ramtlecl  16940  mreexexlem4d  17582  mreexdomd  17584  gsumpropd2lem  18616  gsumzaddlem  19862  gsum2d  19913  telgsums  19934  pgpfac1lem1  20017  pgpfac1lem3a  20019  pgpfac1lem3  20020  pgpfac1lem5  20022  lspsolvlem  21109  lbsextlem2  21126  dsmmacl  21708  eltopss  22863  difopn  22990  tgrest  23115  perfopn  23141  pnfnei  23176  mnfnei  23177  regsep2  23332  cncmp  23348  uncmp  23359  hauscmplem  23362  hauscmp  23363  conndisj  23372  cnconn  23378  conncompss  23389  2ndcctbss  23411  islly2  23440  comppfsc  23488  1stckgenlem  23509  txuni2  23521  ptbasfi  23537  ptpjopn  23568  txindis  23590  txtube  23596  hausdiag  23601  xkoinjcn  23643  tgqtop  23668  filconn  23839  elfm2  23904  flimclslem  23940  flffbas  23951  fclsbas  23977  flimfnfcls  23984  alexsubALT  24007  symgtgp  24062  ustssco  24171  isucn2  24234  ucnima  24236  ucnprima  24237  blcls  24462  prdsxmslem2  24485  isngp2  24553  tgioo  24752  xrtgioo  24763  xrsmopn  24769  opnreen  24788  cnheiborlem  24921  cnllycmp  24923  tcphcph  25205  rrxmvallem  25372  uniioombllem4  25555  dyadmbllem  25568  opnmbllem  25570  mbfimaopnlem  25624  mbflimsup  25635  i1fadd  25664  i1fmul  25665  itg1addlem4  25668  i1fmulc  25672  limciun  25863  dvlip2  25968  c1lip3  25972  lhop  25989  dvfsumlem2  26001  dvfsumlem2OLD  26002  dvfsumrlimge0  26005  dvfsumrlim2  26007  ulmval  26357  psercnlem2  26402  efopnlem2  26634  efopn  26635  madebdayim  27896  madefi  27921  oldfi  27922  addbdaylem  28025  oniso  28279  oldfib  28385  umgrres1lem  29395  upgrres1  29398  nbgrssvwo2  29447  ubthlem1  30957  issh2  31296  mdsymlem1  32490  iunxpssiun1  32654  padct  32807  xrofsup  32857  fz2ssnn0  32875  ccatws1f1o  33043  elrgspnlem1  33335  unitpidl1  33516  mxidlirred  33564  zarclsint  34049  tpr2rico  34089  sibfinima  34516  fct2relem  34774  bnj906  35105  bnj1014  35136  bnj1286  35194  bnj1408  35211  bnj1450  35225  bnj1452  35227  bnj1498  35236  bnj1501  35242  lfuhgr  35331  cvmopnlem  35491  cvmfolem  35492  cvmliftlem6  35503  cvmliftlem8  35505  cvmliftlem13  35509  cvmliftlem15  35511  cvmlift2lem9  35524  cvmlift2lem11  35526  cvmlift2lem12  35527  mclsppslem  35796  filnetlem4  36594  dissneqlem  37589  pibt2  37666  lindsdom  37859  opnmbllem0  37901  cnambfre  37913  heibor1lem  38054  osumcllem1N  40326  osumcllem2N  40327  pexmidlem6N  40345  dochexmidlem6  41835  dochexmidlem7  41836  mapdrvallem3  42016  evlsmhpvvval  42947  naddwordnexlem4  43752  k0004ss2  44502  cpcolld  44608  dvsconst  44680  dvsid  44681  dvsef  44682  iunconnlem2  45284  uzssd2  45769  climinf  45960  climsuse  45962  climresmpt  46011  climleltrp  46028  stoweidlem28  46380  stoweidlem50  46402  stoweidlem52  46404  stoweidlem53  46405  stoweidlem54  46406  fourierdlem54  46512  fourierdlem80  46538  meaiininclem  46838  caratheodorylem2  46879  hspmbllem2  46979  mbfresmf  47091  smfmbfcex  47112  smflimlem2  47124  smflimsuplem2  47173  smflimsuplem3  47174  smflimsuplem5  47176  smflimsuplem6  47177  gpgedgvtx1lem  47685  isuspgrim0  48248  gpgusgralem  48410  upgredgssspr  48497  setrec1  50044  setrecsres  50055  aacllem  50154