Theorem sseqtrrdi 3988

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

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

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 2008  ax-9 2119  ax-ext 2701

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

This theorem is referenced by:  3sstr4g  4000  abssdv  4031  disjxiun  5104  knatar  7332  iunpw  7747  fviunfun  7923  frrlem8  8272  frrlem10  8274  frrlem12  8276  frrlem14  8278  fprresex  8289  tfrlem9  8353  tfrlem9a  8354  tfrlem13  8358  tz7.44-2  8375  tz7.44-3  8376  tz7.49  8413  naddcllem  8640  naddov2  8643  naddasslem1  8658  naddasslem2  8659  marypha1lem  9384  ordtypelem2  9472  ixpiunwdom  9543  oemapvali  9637  tcss  9697  tcel  9698  pwwf  9760  rankpwi  9776  rankval3b  9779  cplem1  9842  dfac12lem2  10098  infmap2  10170  ackbij1b  10191  ttukeylem6  10467  fpwwe2lem10  10593  fpwwe2lem11  10594  fpwwe2lem12  10595  fpwwe2  10596  uznnssnn  12854  pfxccatpfx2  14702  shftfval  15036  rexuzre  15319  climsup  15636  clim2prod  15854  fprodntriv  15908  eulerthlem2  16752  ramtlecl  16971  mreexexlem4d  17608  mreexdomd  17610  gsumpropd2lem  18606  gsumzaddlem  19851  gsum2d  19902  telgsums  19923  pgpfac1lem1  20006  pgpfac1lem3a  20008  pgpfac1lem3  20009  pgpfac1lem5  20011  lspsolvlem  21052  lbsextlem2  21069  dsmmacl  21650  eltopss  22794  difopn  22921  tgrest  23046  perfopn  23072  pnfnei  23107  mnfnei  23108  regsep2  23263  cncmp  23279  uncmp  23290  hauscmplem  23293  hauscmp  23294  conndisj  23303  cnconn  23309  conncompss  23320  2ndcctbss  23342  islly2  23371  comppfsc  23419  1stckgenlem  23440  txuni2  23452  ptbasfi  23468  ptpjopn  23499  txindis  23521  txtube  23527  hausdiag  23532  xkoinjcn  23574  tgqtop  23599  filconn  23770  elfm2  23835  flimclslem  23871  flffbas  23882  fclsbas  23908  flimfnfcls  23915  alexsubALT  23938  symgtgp  23993  ustssco  24102  isucn2  24166  ucnima  24168  ucnprima  24169  blcls  24394  prdsxmslem2  24417  isngp2  24485  tgioo  24684  xrtgioo  24695  xrsmopn  24701  opnreen  24720  cnheiborlem  24853  cnllycmp  24855  tcphcph  25137  rrxmvallem  25304  uniioombllem4  25487  dyadmbllem  25500  opnmbllem  25502  mbfimaopnlem  25556  mbflimsup  25567  i1fadd  25596  i1fmul  25597  itg1addlem4  25600  i1fmulc  25604  limciun  25795  dvlip2  25900  c1lip3  25904  lhop  25921  dvfsumlem2  25933  dvfsumlem2OLD  25934  dvfsumrlimge0  25937  dvfsumrlim2  25939  ulmval  26289  psercnlem2  26334  efopnlem2  26566  efopn  26567  madebdayim  27799  madefi  27824  oldfi  27825  addsbdaylem  27923  onsiso  28169  umgrres1lem  29237  upgrres1  29240  nbgrssvwo2  29289  ubthlem1  30799  issh2  31138  mdsymlem1  32332  iunxpssiun1  32497  padct  32643  xrofsup  32690  fz2ssnn0  32708  ccatws1f1o  32873  elrgspnlem1  33193  unitpidl1  33395  mxidlirred  33443  zarclsint  33862  tpr2rico  33902  sibfinima  34330  fct2relem  34588  bnj906  34920  bnj1014  34951  bnj1286  35009  bnj1408  35026  bnj1450  35040  bnj1452  35042  bnj1498  35051  bnj1501  35057  lfuhgr  35105  cvmopnlem  35265  cvmfolem  35266  cvmliftlem6  35277  cvmliftlem8  35279  cvmliftlem13  35283  cvmliftlem15  35285  cvmlift2lem9  35298  cvmlift2lem11  35300  cvmlift2lem12  35301  mclsppslem  35570  filnetlem4  36369  dissneqlem  37328  pibt2  37405  lindsdom  37608  opnmbllem0  37650  cnambfre  37662  heibor1lem  37803  osumcllem1N  39950  osumcllem2N  39951  pexmidlem6N  39969  dochexmidlem6  41459  dochexmidlem7  41460  mapdrvallem3  41640  evlsmhpvvval  42583  naddwordnexlem4  43390  k0004ss2  44141  cpcolld  44247  dvsconst  44319  dvsid  44320  dvsef  44321  iunconnlem2  44924  uzssd2  45413  climinf  45604  climsuse  45606  climresmpt  45657  climleltrp  45674  stoweidlem28  46026  stoweidlem50  46048  stoweidlem52  46050  stoweidlem53  46051  stoweidlem54  46052  fourierdlem54  46158  fourierdlem80  46184  meaiininclem  46484  caratheodorylem2  46525  hspmbllem2  46625  mbfresmf  46737  smfmbfcex  46758  smflimlem2  46770  smflimsuplem2  46819  smflimsuplem3  46820  smflimsuplem5  46822  smflimsuplem6  46823  gpgedgvtx1lem  47332  isuspgrim0  47894  gpgusgralem  48047  upgredgssspr  48131  setrec1  49680  setrecsres  49691  aacllem  49790