Theorem sseqtrrdi 4032

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3947

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954  df-ss 3964

This theorem is referenced by:  abssdv  4064  disjxiun  5144  knatar  7350  iunpw  7754  fviunfun  7927  frrlem8  8274  frrlem10  8276  frrlem12  8278  frrlem14  8280  fprresex  8291  wfrdmclOLD  8313  wfrlem12OLD  8316  wfrlem16OLD  8320  wfrlem17OLD  8321  tfrlem9  8381  tfrlem9a  8382  tfrlem13  8386  tz7.44-2  8403  tz7.44-3  8404  tz7.49  8441  naddcllem  8671  naddov2  8674  naddasslem1  8689  naddasslem2  8690  marypha1lem  9424  ordtypelem2  9510  ixpiunwdom  9581  oemapvali  9675  tcss  9735  tcel  9736  pwwf  9798  rankpwi  9814  rankval3b  9817  cplem1  9880  dfac12lem2  10135  infmap2  10209  ackbij1b  10230  ttukeylem6  10505  fpwwe2lem10  10631  fpwwe2lem11  10632  fpwwe2lem12  10633  fpwwe2  10634  uznnssnn  12875  pfxccatpfx2  14683  shftfval  15013  rexuzre  15295  climsup  15612  clim2prod  15830  fprodntriv  15882  eulerthlem2  16711  ramtlecl  16929  mreexexlem4d  17587  mreexdomd  17589  gsumpropd2lem  18594  gsumzaddlem  19783  gsum2d  19834  telgsums  19855  pgpfac1lem1  19938  pgpfac1lem3a  19940  pgpfac1lem3  19941  pgpfac1lem5  19943  lspsolvlem  20747  lbsextlem2  20764  dsmmacl  21287  eltopss  22400  difopn  22529  tgrest  22654  perfopn  22680  pnfnei  22715  mnfnei  22716  regsep2  22871  cncmp  22887  uncmp  22898  hauscmplem  22901  hauscmp  22902  conndisj  22911  cnconn  22917  conncompss  22928  2ndcctbss  22950  islly2  22979  comppfsc  23027  1stckgenlem  23048  txuni2  23060  ptbasfi  23076  ptpjopn  23107  txindis  23129  txtube  23135  hausdiag  23140  xkoinjcn  23182  tgqtop  23207  filconn  23378  elfm2  23443  flimclslem  23479  flffbas  23490  fclsbas  23516  flimfnfcls  23523  alexsubALT  23546  symgtgp  23601  ustssco  23710  isucn2  23775  ucnima  23777  ucnprima  23778  blcls  24006  prdsxmslem2  24029  isngp2  24097  tgioo  24303  xrtgioo  24313  xrsmopn  24319  opnreen  24338  cnheiborlem  24461  cnllycmp  24463  tcphcph  24745  rrxmvallem  24912  uniioombllem4  25094  dyadmbllem  25107  opnmbllem  25109  mbfimaopnlem  25163  mbflimsup  25174  i1fadd  25203  i1fmul  25204  itg1addlem4  25207  itg1addlem4OLD  25208  i1fmulc  25212  limciun  25402  dvlip2  25503  c1lip3  25507  lhop  25524  dvfsumlem2  25535  dvfsumrlimge0  25538  dvfsumrlim2  25540  ulmval  25883  psercnlem2  25927  efopnlem2  26156  efopn  26157  madebdayim  27371  umgrres1lem  28556  upgrres1  28559  nbgrssvwo2  28608  ubthlem1  30110  issh2  30449  mdsymlem1  31643  padct  31931  xrofsup  31967  fz2ssnn0  31983  unitpidl1  32530  mxidlirred  32576  zarclsint  32840  tpr2rico  32880  sibfinima  33326  fct2relem  33597  bnj906  33929  bnj1014  33960  bnj1286  34018  bnj1408  34035  bnj1450  34049  bnj1452  34051  bnj1498  34060  bnj1501  34066  lfuhgr  34096  cvmopnlem  34257  cvmfolem  34258  cvmliftlem6  34269  cvmliftlem8  34271  cvmliftlem13  34275  cvmliftlem15  34277  cvmlift2lem9  34290  cvmlift2lem11  34292  cvmlift2lem12  34293  mclsppslem  34562  gg-dvfsumlem2  35171  filnetlem4  35254  dissneqlem  36209  pibt2  36286  lindsdom  36470  opnmbllem0  36512  cnambfre  36524  heibor1lem  36665  osumcllem1N  38815  osumcllem2N  38816  pexmidlem6N  38834  dochexmidlem6  40324  dochexmidlem7  40325  mapdrvallem3  40505  evlsmhpvvval  41164  naddwordnexlem4  42137  k0004ss2  42888  cpcolld  43002  dvsconst  43074  dvsid  43075  dvsef  43076  iunconnlem2  43681  uzssd2  44113  climinf  44308  climsuse  44310  climresmpt  44361  climleltrp  44378  stoweidlem28  44730  stoweidlem50  44752  stoweidlem52  44754  stoweidlem53  44755  stoweidlem54  44756  fourierdlem54  44862  fourierdlem80  44888  meaiininclem  45188  caratheodorylem2  45229  hspmbllem2  45329  mbfresmf  45441  smfmbfcex  45462  smflimlem2  45474  smflimsuplem2  45523  smflimsuplem3  45524  smflimsuplem5  45526  smflimsuplem6  45527  isomuspgrlem2c  46484  upgredgssspr  46507  setrec1  47689  setrecsres  47700  aacllem  47801