Theorem eqsstrid 3976

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 3966	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	sylibr 234	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3905

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 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3922

This theorem is referenced by:  eqsstrrid  3977  3sstr4g  3991  inss  4201  tpssi  4792  opabssxpd  5670  xpsspw  5756  fun  6690  fmpt  7048  fssrescdmd  7064  fliftrel  7249  knatar  7298  fr3nr  7712  ordsuci  7748  sucexeloniOLD  7750  fiun  7885  f1iun  7886  1stcof  7961  2ndcof  7962  fsplitfpar  8058  fnwelem  8071  oeeui  8527  cofon1  8597  aceq3lem  10033  cflecard  10166  cfslb2n  10181  itunitc1  10333  axdc3lem2  10364  fpwwe2lem11  10554  canthwelem  10563  wuncval2  10660  peano5nni  12150  un0addcl  12436  un0mulcl  12437  fsuppmapnn0fiublem  13916  fsuppmapnn0fiub  13917  mertenslem2  15811  4sqlem11  16886  4sqlem19  16894  vdwlem13  16924  imasless  17463  rescfth  17865  oppchofcl  18185  oyoncl  18195  mgmidsssn0  18565  eqg0subg  19094  cycsubm  19100  efgsfo  19637  efgcpbllemb  19653  frgpuplem  19670  gsummpt1n0  19863  dprdfid  19917  dprd2d2  19944  ablfacrp  19966  ablfac1b  19970  ablfac1eu  19973  pgpfac1lem5  19979  ablfaclem3  19987  funcrngcsetc  20544  funcringcsetc  20578  srhmsubc  20584  rhmsubclem3  20591  lsptpcl  20901  lsppratlem3  21075  lsppratlem4  21076  lbsextlem2  21085  f1lindf  21748  topsn  22835  ordtbaslem  23092  ordtuni  23094  ordtbas2  23095  cnpco  23171  cnconst2  23187  tgcmp  23305  iunconn  23332  ptuni2  23480  xkococnlem  23563  tgqtop  23616  fbasrn  23788  uzrest  23801  fmco  23865  alexsubALT  23955  cnextf  23970  snclseqg  24020  ustund  24126  imasdsf1olem  24278  xmetresbl  24342  blsscls2  24409  metustss  24456  tngtopn  24555  reconn  24734  metnrmlem3  24767  cphsubrglem  25094  minveclem1  25341  minveclem3b  25345  ovolficcss  25387  ovolicc2lem4  25438  iundisj2  25467  uniioombllem4  25504  vitalilem5  25530  mbfeqalem1  25559  itg1addlem4  25617  limciun  25812  dvlip2  25917  dv11cn  25923  aalioulem3  26259  pserdvlem2  26355  pserdv  26356  abelthlem2  26359  efif1o  26472  efrlim  26896  efrlimOLD  26897  lgamgulmlem1  26956  fsumdvdsmul  27122  fsumdvdsmulOLD  27124  perfectlem2  27158  noextendseq  27596  nosupno  27632  nosupbnd2lem1  27644  noinfno  27647  noetasuplem4  27665  cuteq1  27767  bdayiun  27848  addsbday  27948  onscutlt  28189  onsiso  28193  bdayn0p1  28282  setsvtx  28999  uhgredgn0  29092  upgredgss  29096  umgredgss  29097  usgredgss  29123  umgrres1lem  29274  upgrres1  29277  1hegrvtxdg1r  29473  clwlknf1oclwwlknlem3  30046  minvecolem1  30837  sh0le  31403  mdslmd3i  32295  iundisj2f  32553  suppss2f  32600  2ndresdju  32611  fnpreimac  32633  fdifsuppconst  32650  suppss3  32686  iundisj2fi  32759  elrgspnsubrunlem1  33206  erlval  33217  lsmsnorb  33347  constrextdg2lem  33734  pstmfval  33882  ordtrest2NEW  33909  ldgenpisyslem1  34149  ldgenpisyslem2  34150  omsmeas  34310  sitgclbn  34330  eulerpartlemt  34358  eulerpartlemmf  34362  eulerpartlemgf  34366  bnj849  34911  bnj1136  34983  bnj1311  35010  bnj1413  35021  bnj1452  35038  blsconn  35236  cvmliftlem2  35278  cvmlift2lem12  35306  mvtss  35545  mthmpps  35574  ellcsrspsn  35633  neibastop2lem  36353  filnetlem3  36373  finxpsuclem  37390  poimirlem3  37622  mblfinlem3  37658  areacirclem2  37708  sdclem1  37742  istotbnd3  37770  sstotbnd  37774  iccbnd  37839  icccmpALT  37840  osumcllem1N  39955  osumcllem2N  39956  osumcllem4N  39958  osumcllem9N  39963  pexmidlem6N  39974  dihglblem3N  41294  dvhdimlem  41443  dochexmidlem6  41464  lcfrlem16  41557  lcfr  41584  aks6d1c6lem3  42165  rhmqusspan  42178  ssabdv  42213  hbtlem6  43122  iocinico  43205  oege2  43300  omabs2  43325  tfsconcatb0  43337  trclubgNEW  43611  cnvrcl0  43618  relexp0a  43709  brtrclfv2  43720  cotrclrcl  43735  frege77d  43739  unhe1  43778  ntrrn  44115  imo72b2lem2  44160  imo72b2  44165  mnuprdlem4  44268  radcnvrat  44307  iunconnlem2  44928  ssinss2d  45058  limccog  45621  limsupresico  45701  liminfresico  45772  icccncfext  45888  stoweidlem14  46015  fourierdlem20  46128  fourierdlem42  46150  fourierdlem46  46153  fourierdlem50  46157  fourierdlem51  46158  fourierdlem54  46161  fourierdlem64  46171  fourierdlem76  46183  fourierdlem102  46209  fourierdlem103  46210  fourierdlem104  46211  fourierdlem114  46221  meadjiunlem  46466  meaiininclem  46487  ovnsupge0  46558  hoidmvlelem2  46597  hoidmvlelem4  46599  vonvolmbllem  46661  vonvolmbl2  46664  vonvol2  46665  vonioolem1  46681  issmflem  46728  fsupdm  46843  finfdm  46847  fundcmpsurinjimaid  47415  perfectALTVlem2  47726  isubgruhgr  47872  uspgropssxp  48148  rhmsubcALTVlem4  48288  srhmsubcALTV  48329  imasubc  49156  imassc  49158  setrec2fun  49697  onsetreclem2  49711