Theorem eqsstrid 4031

Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
eqsstrid.1	⊢ 𝐴 = 𝐵
eqsstrid.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
eqsstrid	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem eqsstrid

Step	Hyp	Ref	Expression
1		eqsstrid.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
2		eqsstrid.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	sseq1i 4011	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	sylibr 233	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956  df-ss 3966

This theorem is referenced by:  eqsstrrid  4032  inss  4239  tpssi  4840  opabssxpd  5724  xpsspw  5810  fun  6754  fmpt  7110  fliftrel  7305  knatar  7354  fr3nr  7759  ordsuci  7796  sucexeloniOLD  7798  suceloniOLD  7800  fiun  7929  f1iun  7930  1stcof  8005  2ndcof  8006  fsplitfpar  8104  fnwelem  8117  oeeui  8602  cofon1  8671  aceq3lem  10115  cflecard  10248  cfslb2n  10263  itunitc1  10415  axdc3lem2  10446  fpwwe2lem11  10636  canthwelem  10645  wuncval2  10742  peano5nni  12215  un0addcl  12505  un0mulcl  12506  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  mertenslem2  15831  4sqlem11  16888  4sqlem19  16896  vdwlem13  16926  imasless  17486  rescfth  17888  oppchofcl  18213  oyoncl  18223  mgmidsssn0  18591  eqg0subg  19073  cycsubm  19079  efgsfo  19607  efgcpbllemb  19623  frgpuplem  19640  gsummpt1n0  19833  dprdfid  19887  dprd2d2  19914  ablfacrp  19936  ablfac1b  19940  ablfac1eu  19943  pgpfac1lem5  19949  ablfaclem3  19957  lsptpcl  20590  lsppratlem3  20762  lsppratlem4  20763  lbsextlem2  20772  f1lindf  21377  topsn  22433  ordtbaslem  22692  ordtuni  22694  ordtbas2  22695  cnpco  22771  cnconst2  22787  tgcmp  22905  iunconn  22932  ptuni2  23080  xkococnlem  23163  tgqtop  23216  fbasrn  23388  uzrest  23401  fmco  23465  alexsubALT  23555  cnextf  23570  snclseqg  23620  ustund  23726  imasdsf1olem  23879  xmetresbl  23943  blsscls2  24013  metustss  24060  tngtopn  24167  reconn  24344  metnrmlem3  24377  cphsubrglem  24694  minveclem1  24941  minveclem3b  24945  ovolficcss  24986  ovolicc2lem4  25037  iundisj2  25066  uniioombllem4  25103  vitalilem5  25129  mbfeqalem1  25158  itg1addlem4  25216  itg1addlem4OLD  25217  limciun  25411  dvlip2  25512  dv11cn  25518  aalioulem3  25847  pserdvlem2  25940  pserdv  25941  abelthlem2  25944  efif1o  26055  efrlim  26474  lgamgulmlem1  26533  fsumdvdsmul  26699  perfectlem2  26733  noextendseq  27170  nosupno  27206  nosupbnd2lem1  27218  noinfno  27221  noetasuplem4  27239  cuteq1  27334  setsvtx  28295  uhgredgn0  28388  upgredgss  28392  umgredgss  28393  usgredgss  28419  umgrres1lem  28567  upgrres1  28570  1hegrvtxdg1r  28765  clwlknf1oclwwlknlem3  29336  minvecolem1  30127  sh0le  30693  mdslmd3i  31585  iundisj2f  31821  suppss2f  31863  2ndresdju  31874  fnpreimac  31896  fdifsuppconst  31911  suppss3  31949  iundisj2fi  32008  lsmsnorb  32501  pstmfval  32876  ordtrest2NEW  32903  ldgenpisyslem1  33161  ldgenpisyslem2  33162  omsmeas  33322  sitgclbn  33342  eulerpartlemt  33370  eulerpartlemmf  33374  eulerpartlemgf  33378  bnj849  33936  bnj1136  34008  bnj1311  34035  bnj1413  34046  bnj1452  34063  blsconn  34235  cvmliftlem2  34277  cvmlift2lem12  34305  mvtss  34544  mthmpps  34573  neibastop2lem  35245  filnetlem3  35265  finxpsuclem  36278  poimirlem3  36491  mblfinlem3  36527  areacirclem2  36577  sdclem1  36611  istotbnd3  36639  sstotbnd  36643  iccbnd  36708  icccmpALT  36709  osumcllem1N  38827  osumcllem2N  38828  osumcllem4N  38830  osumcllem9N  38835  pexmidlem6N  38846  dihglblem3N  40166  dvhdimlem  40315  dochexmidlem6  40336  lcfrlem16  40429  lcfr  40456  ssabdv  41037  hbtlem6  41871  iocinico  41961  oege2  42057  omabs2  42082  tfsconcatb0  42094  trclubgNEW  42369  cnvrcl0  42376  relexp0a  42467  brtrclfv2  42478  cotrclrcl  42493  frege77d  42497  unhe1  42536  ntrrn  42873  imo72b2lem0  42917  imo72b2lem2  42919  imo72b2  42924  mnuprdlem4  43034  radcnvrat  43073  iunconnlem2  43696  ssinss2d  43747  limccog  44336  limsupresico  44416  liminfresico  44487  icccncfext  44603  stoweidlem14  44730  fourierdlem20  44843  fourierdlem42  44865  fourierdlem46  44868  fourierdlem50  44872  fourierdlem51  44873  fourierdlem54  44876  fourierdlem64  44886  fourierdlem76  44898  fourierdlem102  44924  fourierdlem103  44925  fourierdlem104  44926  fourierdlem114  44936  meadjiunlem  45181  meaiininclem  45202  ovnsupge0  45273  hoidmvlelem2  45312  hoidmvlelem4  45314  vonvolmbllem  45376  vonvolmbl2  45379  vonvol2  45380  vonioolem1  45396  issmflem  45443  fsupdm  45558  finfdm  45562  fundcmpsurinjimaid  46079  perfectALTVlem2  46390  uspgropssxp  46522  funcrngcsetc  46896  funcringcsetc  46933  srhmsubc  46974  rhmsubclem3  46986  srhmsubcALTV  46992  rhmsubcALTVlem4  47005  setrec2fun  47737  onsetreclem2  47751