Theorem sseqtrrdi 3972

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  3sstr4g  3984  abssdv  4016  disjxiun  5090  knatar  7297  iunpw  7710  fviunfun  7883  frrlem8  8229  frrlem10  8231  frrlem12  8233  frrlem14  8235  fprresex  8246  tfrlem9  8310  tfrlem9a  8311  tfrlem13  8315  tz7.44-2  8332  tz7.44-3  8333  tz7.49  8370  naddcllem  8597  naddov2  8600  naddasslem1  8615  naddasslem2  8616  marypha1lem  9324  ordtypelem2  9412  ixpiunwdom  9483  oemapvali  9581  tcss  9639  tcel  9640  pwwf  9707  rankpwi  9723  rankval3b  9726  cplem1  9789  dfac12lem2  10043  infmap2  10115  ackbij1b  10136  ttukeylem6  10412  fpwwe2lem10  10538  fpwwe2lem11  10539  fpwwe2lem12  10540  fpwwe2  10541  uznnssnn  12795  pfxccatpfx2  14646  shftfval  14979  rexuzre  15262  climsup  15579  clim2prod  15797  fprodntriv  15851  eulerthlem2  16695  ramtlecl  16914  mreexexlem4d  17555  mreexdomd  17557  gsumpropd2lem  18589  gsumzaddlem  19835  gsum2d  19886  telgsums  19907  pgpfac1lem1  19990  pgpfac1lem3a  19992  pgpfac1lem3  19993  pgpfac1lem5  19995  lspsolvlem  21081  lbsextlem2  21098  dsmmacl  21680  eltopss  22823  difopn  22950  tgrest  23075  perfopn  23101  pnfnei  23136  mnfnei  23137  regsep2  23292  cncmp  23308  uncmp  23319  hauscmplem  23322  hauscmp  23323  conndisj  23332  cnconn  23338  conncompss  23349  2ndcctbss  23371  islly2  23400  comppfsc  23448  1stckgenlem  23469  txuni2  23481  ptbasfi  23497  ptpjopn  23528  txindis  23550  txtube  23556  hausdiag  23561  xkoinjcn  23603  tgqtop  23628  filconn  23799  elfm2  23864  flimclslem  23900  flffbas  23911  fclsbas  23937  flimfnfcls  23944  alexsubALT  23967  symgtgp  24022  ustssco  24131  isucn2  24194  ucnima  24196  ucnprima  24197  blcls  24422  prdsxmslem2  24445  isngp2  24513  tgioo  24712  xrtgioo  24723  xrsmopn  24729  opnreen  24748  cnheiborlem  24881  cnllycmp  24883  tcphcph  25165  rrxmvallem  25332  uniioombllem4  25515  dyadmbllem  25528  opnmbllem  25530  mbfimaopnlem  25584  mbflimsup  25595  i1fadd  25624  i1fmul  25625  itg1addlem4  25628  i1fmulc  25632  limciun  25823  dvlip2  25928  c1lip3  25932  lhop  25949  dvfsumlem2  25961  dvfsumlem2OLD  25962  dvfsumrlimge0  25965  dvfsumrlim2  25967  ulmval  26317  psercnlem2  26362  efopnlem2  26594  efopn  26595  madebdayim  27834  madefi  27859  oldfi  27860  addsbdaylem  27960  onsiso  28206  umgrres1lem  29290  upgrres1  29293  nbgrssvwo2  29342  ubthlem1  30852  issh2  31191  mdsymlem1  32385  iunxpssiun1  32550  padct  32705  xrofsup  32754  fz2ssnn0  32772  ccatws1f1o  32939  elrgspnlem1  33216  unitpidl1  33396  mxidlirred  33444  zarclsint  33906  tpr2rico  33946  sibfinima  34373  fct2relem  34631  bnj906  34963  bnj1014  34994  bnj1286  35052  bnj1408  35069  bnj1450  35083  bnj1452  35085  bnj1498  35094  bnj1501  35100  lfuhgr  35183  cvmopnlem  35343  cvmfolem  35344  cvmliftlem6  35355  cvmliftlem8  35357  cvmliftlem13  35361  cvmliftlem15  35363  cvmlift2lem9  35376  cvmlift2lem11  35378  cvmlift2lem12  35379  mclsppslem  35648  filnetlem4  36446  dissneqlem  37405  pibt2  37482  lindsdom  37674  opnmbllem0  37716  cnambfre  37728  heibor1lem  37869  osumcllem1N  40075  osumcllem2N  40076  pexmidlem6N  40094  dochexmidlem6  41584  dochexmidlem7  41585  mapdrvallem3  41765  evlsmhpvvval  42713  naddwordnexlem4  43518  k0004ss2  44269  cpcolld  44375  dvsconst  44447  dvsid  44448  dvsef  44449  iunconnlem2  45051  uzssd2  45539  climinf  45730  climsuse  45732  climresmpt  45781  climleltrp  45798  stoweidlem28  46150  stoweidlem50  46172  stoweidlem52  46174  stoweidlem53  46175  stoweidlem54  46176  fourierdlem54  46282  fourierdlem80  46308  meaiininclem  46608  caratheodorylem2  46649  hspmbllem2  46749  mbfresmf  46861  smfmbfcex  46882  smflimlem2  46894  smflimsuplem2  46943  smflimsuplem3  46944  smflimsuplem5  46946  smflimsuplem6  46947  gpgedgvtx1lem  47455  isuspgrim0  48018  gpgusgralem  48180  upgredgssspr  48267  setrec1  49816  setrecsres  49827  aacllem  49926