Theorem sseqtrrdi 3963

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

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

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 2708

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

This theorem is referenced by:  3sstr4g  3975  abssdv  4007  disjxiun  5082  knatar  7312  iunpw  7725  fviunfun  7898  frrlem8  8243  frrlem10  8245  frrlem12  8247  frrlem14  8249  fprresex  8260  tfrlem9  8324  tfrlem9a  8325  tfrlem13  8329  tz7.44-2  8346  tz7.44-3  8347  tz7.49  8384  naddcllem  8612  naddov2  8615  naddasslem1  8630  naddasslem2  8631  marypha1lem  9346  ordtypelem2  9434  ixpiunwdom  9505  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  12845  pfxccatpfx2  14699  shftfval  15032  rexuzre  15315  climsup  15632  clim2prod  15853  fprodntriv  15907  eulerthlem2  16752  ramtlecl  16971  mreexexlem4d  17613  mreexdomd  17615  gsumpropd2lem  18647  gsumzaddlem  19896  gsum2d  19947  telgsums  19968  pgpfac1lem1  20051  pgpfac1lem3a  20053  pgpfac1lem3  20054  pgpfac1lem5  20056  lspsolvlem  21140  lbsextlem2  21157  dsmmacl  21721  eltopss  22872  difopn  22999  tgrest  23124  perfopn  23150  pnfnei  23185  mnfnei  23186  regsep2  23341  cncmp  23357  uncmp  23368  hauscmplem  23371  hauscmp  23372  conndisj  23381  cnconn  23387  conncompss  23398  2ndcctbss  23420  islly2  23449  comppfsc  23497  1stckgenlem  23518  txuni2  23530  ptbasfi  23546  ptpjopn  23577  txindis  23599  txtube  23605  hausdiag  23610  xkoinjcn  23652  tgqtop  23677  filconn  23848  elfm2  23913  flimclslem  23949  flffbas  23960  fclsbas  23986  flimfnfcls  23993  alexsubALT  24016  symgtgp  24071  ustssco  24180  isucn2  24243  ucnima  24245  ucnprima  24246  blcls  24471  prdsxmslem2  24494  isngp2  24562  tgioo  24761  xrtgioo  24772  xrsmopn  24778  opnreen  24797  cnheiborlem  24921  cnllycmp  24923  tcphcph  25204  rrxmvallem  25371  uniioombllem4  25553  dyadmbllem  25566  opnmbllem  25568  mbfimaopnlem  25622  mbflimsup  25633  i1fadd  25662  i1fmul  25663  itg1addlem4  25666  i1fmulc  25670  limciun  25861  dvlip2  25962  c1lip3  25966  lhop  25983  dvfsumlem2  25994  dvfsumrlimge0  25997  dvfsumrlim2  25999  ulmval  26345  psercnlem2  26389  efopnlem2  26621  efopn  26622  madebdayim  27880  madefi  27905  oldfi  27906  addbdaylem  28009  oniso  28263  oldfib  28369  umgrres1lem  29379  upgrres1  29382  nbgrssvwo2  29431  ubthlem1  30941  issh2  31280  mdsymlem1  32474  iunxpssiun1  32638  padct  32791  xrofsup  32840  fz2ssnn0  32858  ccatws1f1o  33011  elrgspnlem1  33303  unitpidl1  33484  mxidlirred  33532  zarclsint  34016  tpr2rico  34056  sibfinima  34483  fct2relem  34741  bnj906  35072  bnj1014  35103  bnj1286  35161  bnj1408  35178  bnj1450  35192  bnj1452  35194  bnj1498  35203  bnj1501  35209  lfuhgr  35300  cvmopnlem  35460  cvmfolem  35461  cvmliftlem6  35472  cvmliftlem8  35474  cvmliftlem13  35478  cvmliftlem15  35480  cvmlift2lem9  35493  cvmlift2lem11  35495  cvmlift2lem12  35496  mclsppslem  35765  filnetlem4  36563  dissneqlem  37656  pibt2  37733  lindsdom  37935  opnmbllem0  37977  cnambfre  37989  heibor1lem  38130  osumcllem1N  40402  osumcllem2N  40403  pexmidlem6N  40421  dochexmidlem6  41911  dochexmidlem7  41912  mapdrvallem3  42092  evlsmhpvvval  43028  naddwordnexlem4  43829  k0004ss2  44579  cpcolld  44685  dvsconst  44757  dvsid  44758  dvsef  44759  iunconnlem2  45361  uzssd2  45845  climinf  46036  climsuse  46038  climresmpt  46087  climleltrp  46104  stoweidlem28  46456  stoweidlem50  46478  stoweidlem52  46480  stoweidlem53  46481  stoweidlem54  46482  fourierdlem54  46588  fourierdlem80  46614  meaiininclem  46914  caratheodorylem2  46955  hspmbllem2  47055  mbfresmf  47167  smfmbfcex  47188  smflimlem2  47200  smflimsuplem2  47249  smflimsuplem3  47250  smflimsuplem5  47252  smflimsuplem6  47253  gpgedgvtx1lem  47783  isuspgrim0  48370  gpgusgralem  48532  upgredgssspr  48619  setrec1  50166  setrecsres  50177  aacllem  50276