Theorem sseqtrrdi 3973

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895  df-ss 3905

This theorem is referenced by:  disjxiun  5072  knatar  7237  iunpw  7630  fviunfun  7796  frrlem8  8118  frrlem10  8120  frrlem12  8122  frrlem14  8124  fprresex  8135  wfrdmclOLD  8157  wfrlem12OLD  8160  wfrlem16OLD  8164  wfrlem17OLD  8165  tfrlem9  8225  tfrlem9a  8226  tfrlem13  8230  tz7.44-2  8247  tz7.44-3  8248  tz7.49  8285  marypha1lem  9201  ordtypelem2  9287  ixpiunwdom  9358  oemapvali  9451  tcss  9511  tcel  9512  pwwf  9574  rankpwi  9590  rankval3b  9593  cplem1  9656  dfac12lem2  9909  infmap2  9983  ackbij1b  10004  ttukeylem6  10279  fpwwe2lem10  10405  fpwwe2lem11  10406  fpwwe2lem12  10407  fpwwe2  10408  uznnssnn  12644  pfxccatpfx2  14459  shftfval  14790  rexuzre  15073  climsup  15390  clim2prod  15609  fprodntriv  15661  eulerthlem2  16492  ramtlecl  16710  mreexexlem4d  17365  mreexdomd  17367  gsumpropd2lem  18372  gsumzaddlem  19531  gsum2d  19582  telgsums  19603  pgpfac1lem1  19686  pgpfac1lem3a  19688  pgpfac1lem3  19689  pgpfac1lem5  19691  lspsolvlem  20413  lbsextlem2  20430  dsmmacl  20957  eltopss  22065  difopn  22194  tgrest  22319  perfopn  22345  pnfnei  22380  mnfnei  22381  regsep2  22536  cncmp  22552  uncmp  22563  hauscmplem  22566  hauscmp  22567  conndisj  22576  cnconn  22582  conncompss  22593  2ndcctbss  22615  islly2  22644  comppfsc  22692  1stckgenlem  22713  txuni2  22725  ptbasfi  22741  ptpjopn  22772  txindis  22794  txtube  22800  hausdiag  22805  xkoinjcn  22847  tgqtop  22872  filconn  23043  elfm2  23108  flimclslem  23144  flffbas  23155  fclsbas  23181  flimfnfcls  23188  alexsubALT  23211  symgtgp  23266  ustssco  23375  isucn2  23440  ucnima  23442  ucnprima  23443  blcls  23671  prdsxmslem2  23694  isngp2  23762  tgioo  23968  xrtgioo  23978  xrsmopn  23984  opnreen  24003  cnheiborlem  24126  cnllycmp  24128  tcphcph  24410  rrxmvallem  24577  uniioombllem4  24759  dyadmbllem  24772  opnmbllem  24774  mbfimaopnlem  24828  mbflimsup  24839  i1fadd  24868  i1fmul  24869  itg1addlem4  24872  itg1addlem4OLD  24873  i1fmulc  24877  limciun  25067  dvlip2  25168  c1lip3  25172  lhop  25189  dvfsumlem2  25200  dvfsumrlimge0  25203  dvfsumrlim2  25205  ulmval  25548  psercnlem2  25592  efopnlem2  25821  efopn  25822  umgrres1lem  27686  upgrres1  27689  nbgrssvwo2  27738  ubthlem1  29241  issh2  29580  mdsymlem1  30774  padct  31063  xrofsup  31099  fz2ssnn0  31115  zarclsint  31831  tpr2rico  31871  sibfinima  32315  fct2relem  32586  bnj906  32919  bnj1014  32950  bnj1286  33008  bnj1408  33025  bnj1450  33039  bnj1452  33041  bnj1498  33050  bnj1501  33056  lfuhgr  33088  cvmopnlem  33249  cvmfolem  33250  cvmliftlem6  33261  cvmliftlem8  33263  cvmliftlem13  33267  cvmliftlem15  33269  cvmlift2lem9  33282  cvmlift2lem11  33284  cvmlift2lem12  33285  mclsppslem  33554  naddcllem  33840  naddov2  33843  madebdayim  34079  filnetlem4  34579  dissneqlem  35520  pibt2  35597  lindsdom  35780  opnmbllem0  35822  cnambfre  35834  heibor1lem  35976  osumcllem1N  37977  osumcllem2N  37978  pexmidlem6N  37996  dochexmidlem6  39486  dochexmidlem7  39487  mapdrvallem3  39667  k0004ss2  41769  cpcolld  41883  dvsconst  41955  dvsid  41956  dvsef  41957  iunconnlem2  42562  uzssd2  42964  climinf  43154  climsuse  43156  climresmpt  43207  climleltrp  43224  stoweidlem28  43576  stoweidlem50  43598  stoweidlem52  43600  stoweidlem53  43601  stoweidlem54  43602  fourierdlem54  43708  fourierdlem80  43734  meaiininclem  44031  caratheodorylem2  44072  hspmbllem2  44172  mbfresmf  44284  smfmbfcex  44305  smflimlem2  44317  smflimsuplem2  44365  smflimsuplem3  44366  smflimsuplem5  44368  smflimsuplem6  44369  isomuspgrlem2c  45293  upgredgssspr  45316  setrec1  46408  setrecsres  46418  aacllem  46516