Theorem sseqtrrdi 3980

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

Syntax hints:   → wi 4   = wceq 1563   ⊆ wss 3907

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1803  df-cleq 2757  df-ss 3924

This theorem is referenced by:  3sstr4g  3992  abssdv  4023  disjxiun  5102  knatar  7345  iunpw  7758  fviunfun  7930  frrlem8  8278  frrlem10  8280  frrlem12  8282  frrlem14  8284  fprresex  8295  tfrlem9  8360  tfrlem9a  8361  tfrlem13  8365  tz7.44-2  8382  tz7.44-3  8383  tz7.49  8420  naddcllem  8650  naddov2  8653  naddasslem1  8669  naddasslem2  8670  marypha1lem  9381  ordtypelem2  9469  ixpiunwdom  9540  oemapvali  9641  tcss  9699  tcel  9700  pwwf  9767  rankpwi  9783  rankval3b  9786  cplem1  9863  dfac12lem2  10116  infmap2  10188  ackbij1b  10209  ttukeylem6  10486  fpwwe2lem10  10613  fpwwe2lem11  10614  fpwwe2lem12  10615  fpwwe2  10616  uznnssnn  12910  pfxccatpfx2  14764  shftfval  15097  rexuzre  15394  climsup  15711  clim2prod  15932  fprodntriv  15986  eulerthlem2  16831  ramtlecl  17050  mreexexlem4d  17693  mreexdomd  17695  gsumpropd2lem  18727  gsumzaddlem  19982  gsum2d  20033  telgsums  20054  pgpfac1lem1  20137  pgpfac1lem3a  20139  pgpfac1lem3  20140  pgpfac1lem5  20142  lspsolvlem  21235  lbsextlem2  21252  dsmmacl  21851  eltopss  23025  difopn  23152  tgrest  23277  perfopn  23303  pnfnei  23338  mnfnei  23339  regsep2  23494  cncmp  23510  uncmp  23521  hauscmplem  23524  hauscmp  23525  conndisj  23534  cnconn  23540  conncompss  23551  2ndcctbss  23573  islly2  23602  comppfsc  23650  1stckgenlem  23671  txuni2  23683  ptbasfi  23699  ptpjopn  23730  txindis  23752  txtube  23758  hausdiag  23763  xkoinjcn  23805  tgqtop  23830  filconn  24001  elfm2  24066  flimclslem  24102  flffbas  24113  fclsbas  24139  flimfnfcls  24146  alexsubALT  24169  symgtgp  24224  ustssco  24333  isucn2  24396  ucnima  24398  ucnprima  24399  blcls  24624  prdsxmslem2  24647  isngp2  24715  tgioo  24914  xrtgioo  24925  xrsmopn  24931  opnreen  24950  cnheiborlem  25074  cnllycmp  25076  tcphcph  25357  rrxmvallem  25524  uniioombllem4  25706  dyadmbllem  25719  opnmbllem  25721  mbfimaopnlem  25775  mbflimsup  25786  i1fadd  25815  i1fmul  25816  itg1addlem4  25819  i1fmulc  25823  limciun  26014  dvlip2  26115  c1lip3  26119  lhop  26136  dvfsumlem2  26147  dvfsumrlimge0  26150  dvfsumrlim2  26152  ulmval  26501  psercnlem2  26545  efopnlem2  26780  efopn  26781  madebdayim  28039  madefi  28064  oldfi  28065  addbdaylem  28168  oniso  28422  oldfib  28528  umgrres1lem  29569  upgrres1  29572  nbgrssvwo2  29621  ubthlem1  31131  issh2  31470  mdsymlem1  32664  iunxpssiun1  32823  padct  32975  xrofsup  33024  fz2ssnn0  33042  ccatws1f1o  33184  elrgspnlem1  33475  unitpidl1  33648  mxidlirred  33672  zarclsint  34179  tpr2rico  34219  sibfinima  34646  fct2relem  34901  bnj906  35235  bnj1014  35266  bnj1286  35324  bnj1408  35341  bnj1450  35355  bnj1452  35357  bnj1498  35366  bnj1501  35372  vonf1oonfo  35470  lfuhgr  35481  cvmopnlem  35641  cvmfolem  35642  cvmliftlem6  35653  cvmliftlem8  35655  cvmliftlem13  35659  cvmliftlem15  35661  cvmlift2lem9  35674  cvmlift2lem11  35676  cvmlift2lem12  35677  mclsppslem  35946  filnetlem4  36754  dissneqlem  37846  pibt2  37923  lindsdom  38125  opnmbllem0  38167  cnambfre  38179  heibor1lem  38320  osumcllem1N  40592  osumcllem2N  40593  pexmidlem6N  40611  dochexmidlem6  42101  dochexmidlem7  42102  mapdrvallem3  42282  evlsmhpvvval  43189  naddwordnexlem4  43990  k0004ss2  44740  cpcolld  44832  dvsconst  44904  dvsid  44905  dvsef  44906  iunconnlem2  45508  uzssd2  45989  climinf  46180  climsuse  46182  climresmpt  46231  climleltrp  46248  stoweidlem28  46600  stoweidlem50  46622  stoweidlem52  46624  stoweidlem53  46625  stoweidlem54  46626  fourierdlem54  46732  fourierdlem80  46758  meaiininclem  47058  caratheodorylem2  47099  hspmbllem2  47199  mbfresmf  47311  smfmbfcex  47332  smflimlem2  47344  smflimsuplem2  47393  smflimsuplem3  47394  smflimsuplem5  47396  smflimsuplem6  47397  gpgedgvtx1lem  47927  isuspgrim0  48514  gpgusgralem  48676  upgredgssspr  48763  setrec1  50320  setrecsres  50331  aacllem  50430