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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-tru 1542  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-in 3954  df-ss 3964

This theorem is referenced by:  abssdv  4064  disjxiun  5144  knatar  7356  iunpw  7760  fviunfun  7933  frrlem8  8280  frrlem10  8282  frrlem12  8284  frrlem14  8286  fprresex  8297  wfrdmclOLD  8319  wfrlem12OLD  8322  wfrlem16OLD  8326  wfrlem17OLD  8327  tfrlem9  8387  tfrlem9a  8388  tfrlem13  8392  tz7.44-2  8409  tz7.44-3  8410  tz7.49  8447  naddcllem  8677  naddov2  8680  naddasslem1  8695  naddasslem2  8696  marypha1lem  9430  ordtypelem2  9516  ixpiunwdom  9587  oemapvali  9681  tcss  9741  tcel  9742  pwwf  9804  rankpwi  9820  rankval3b  9823  cplem1  9886  dfac12lem2  10141  infmap2  10215  ackbij1b  10236  ttukeylem6  10511  fpwwe2lem10  10637  fpwwe2lem11  10638  fpwwe2lem12  10639  fpwwe2  10640  uznnssnn  12883  pfxccatpfx2  14691  shftfval  15021  rexuzre  15303  climsup  15620  clim2prod  15838  fprodntriv  15890  eulerthlem2  16719  ramtlecl  16937  mreexexlem4d  17595  mreexdomd  17597  gsumpropd2lem  18604  gsumzaddlem  19830  gsum2d  19881  telgsums  19902  pgpfac1lem1  19985  pgpfac1lem3a  19987  pgpfac1lem3  19988  pgpfac1lem5  19990  lspsolvlem  20900  lbsextlem2  20917  dsmmacl  21515  eltopss  22629  difopn  22758  tgrest  22883  perfopn  22909  pnfnei  22944  mnfnei  22945  regsep2  23100  cncmp  23116  uncmp  23127  hauscmplem  23130  hauscmp  23131  conndisj  23140  cnconn  23146  conncompss  23157  2ndcctbss  23179  islly2  23208  comppfsc  23256  1stckgenlem  23277  txuni2  23289  ptbasfi  23305  ptpjopn  23336  txindis  23358  txtube  23364  hausdiag  23369  xkoinjcn  23411  tgqtop  23436  filconn  23607  elfm2  23672  flimclslem  23708  flffbas  23719  fclsbas  23745  flimfnfcls  23752  alexsubALT  23775  symgtgp  23830  ustssco  23939  isucn2  24004  ucnima  24006  ucnprima  24007  blcls  24235  prdsxmslem2  24258  isngp2  24326  tgioo  24532  xrtgioo  24542  xrsmopn  24548  opnreen  24567  cnheiborlem  24700  cnllycmp  24702  tcphcph  24985  rrxmvallem  25152  uniioombllem4  25335  dyadmbllem  25348  opnmbllem  25350  mbfimaopnlem  25404  mbflimsup  25415  i1fadd  25444  i1fmul  25445  itg1addlem4  25448  itg1addlem4OLD  25449  i1fmulc  25453  limciun  25643  dvlip2  25747  c1lip3  25751  lhop  25768  dvfsumlem2  25779  dvfsumrlimge0  25782  dvfsumrlim2  25784  ulmval  26128  psercnlem2  26172  efopnlem2  26401  efopn  26402  madebdayim  27619  umgrres1lem  28834  upgrres1  28837  nbgrssvwo2  28886  ubthlem1  30390  issh2  30729  mdsymlem1  31923  padct  32211  xrofsup  32247  fz2ssnn0  32263  unitpidl1  32816  mxidlirred  32862  zarclsint  33150  tpr2rico  33190  sibfinima  33636  fct2relem  33907  bnj906  34239  bnj1014  34270  bnj1286  34328  bnj1408  34345  bnj1450  34359  bnj1452  34361  bnj1498  34370  bnj1501  34376  lfuhgr  34406  cvmopnlem  34567  cvmfolem  34568  cvmliftlem6  34579  cvmliftlem8  34581  cvmliftlem13  34585  cvmliftlem15  34587  cvmlift2lem9  34600  cvmlift2lem11  34602  cvmlift2lem12  34603  mclsppslem  34872  gg-dvfsumlem2  35469  filnetlem4  35569  dissneqlem  36524  pibt2  36601  lindsdom  36785  opnmbllem0  36827  cnambfre  36839  heibor1lem  36980  osumcllem1N  39130  osumcllem2N  39131  pexmidlem6N  39149  dochexmidlem6  40639  dochexmidlem7  40640  mapdrvallem3  40820  evlsmhpvvval  41469  naddwordnexlem4  42454  k0004ss2  43205  cpcolld  43319  dvsconst  43391  dvsid  43392  dvsef  43393  iunconnlem2  43998  uzssd2  44425  climinf  44620  climsuse  44622  climresmpt  44673  climleltrp  44690  stoweidlem28  45042  stoweidlem50  45064  stoweidlem52  45066  stoweidlem53  45067  stoweidlem54  45068  fourierdlem54  45174  fourierdlem80  45200  meaiininclem  45500  caratheodorylem2  45541  hspmbllem2  45641  mbfresmf  45753  smfmbfcex  45774  smflimlem2  45786  smflimsuplem2  45835  smflimsuplem3  45836  smflimsuplem5  45838  smflimsuplem6  45839  isomuspgrlem2c  46796  upgredgssspr  46819  setrec1  47823  setrecsres  47834  aacllem  47935