Theorem eqsstrid 3988

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

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

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 2702

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

This theorem is referenced by:  eqsstrrid  3989  3sstr4g  4003  inss  4214  tpssi  4805  opabssxpd  5688  xpsspw  5775  fun  6725  fmpt  7085  fssrescdmd  7101  fliftrel  7286  knatar  7335  fr3nr  7751  ordsuci  7787  sucexeloniOLD  7789  fiun  7924  f1iun  7925  1stcof  8001  2ndcof  8002  fsplitfpar  8100  fnwelem  8113  oeeui  8569  cofon1  8639  aceq3lem  10080  cflecard  10213  cfslb2n  10228  itunitc1  10380  axdc3lem2  10411  fpwwe2lem11  10601  canthwelem  10610  wuncval2  10707  peano5nni  12196  un0addcl  12482  un0mulcl  12483  fsuppmapnn0fiublem  13962  fsuppmapnn0fiub  13963  mertenslem2  15858  4sqlem11  16933  4sqlem19  16941  vdwlem13  16971  imasless  17510  rescfth  17908  oppchofcl  18228  oyoncl  18238  mgmidsssn0  18606  eqg0subg  19135  cycsubm  19141  efgsfo  19676  efgcpbllemb  19692  frgpuplem  19709  gsummpt1n0  19902  dprdfid  19956  dprd2d2  19983  ablfacrp  20005  ablfac1b  20009  ablfac1eu  20012  pgpfac1lem5  20018  ablfaclem3  20026  funcrngcsetc  20556  funcringcsetc  20590  srhmsubc  20596  rhmsubclem3  20603  lsptpcl  20892  lsppratlem3  21066  lsppratlem4  21067  lbsextlem2  21076  f1lindf  21738  topsn  22825  ordtbaslem  23082  ordtuni  23084  ordtbas2  23085  cnpco  23161  cnconst2  23177  tgcmp  23295  iunconn  23322  ptuni2  23470  xkococnlem  23553  tgqtop  23606  fbasrn  23778  uzrest  23791  fmco  23855  alexsubALT  23945  cnextf  23960  snclseqg  24010  ustund  24116  imasdsf1olem  24268  xmetresbl  24332  blsscls2  24399  metustss  24446  tngtopn  24545  reconn  24724  metnrmlem3  24757  cphsubrglem  25084  minveclem1  25331  minveclem3b  25335  ovolficcss  25377  ovolicc2lem4  25428  iundisj2  25457  uniioombllem4  25494  vitalilem5  25520  mbfeqalem1  25549  itg1addlem4  25607  limciun  25802  dvlip2  25907  dv11cn  25913  aalioulem3  26249  pserdvlem2  26345  pserdv  26346  abelthlem2  26349  efif1o  26462  efrlim  26886  efrlimOLD  26887  lgamgulmlem1  26946  fsumdvdsmul  27112  fsumdvdsmulOLD  27114  perfectlem2  27148  noextendseq  27586  nosupno  27622  nosupbnd2lem1  27634  noinfno  27637  noetasuplem4  27655  cuteq1  27753  addsbday  27931  onscutlt  28172  onsiso  28176  bdayn0p1  28265  setsvtx  28969  uhgredgn0  29062  upgredgss  29066  umgredgss  29067  usgredgss  29093  umgrres1lem  29244  upgrres1  29247  1hegrvtxdg1r  29443  clwlknf1oclwwlknlem3  30019  minvecolem1  30810  sh0le  31376  mdslmd3i  32268  iundisj2f  32526  suppss2f  32569  2ndresdju  32580  fnpreimac  32602  fdifsuppconst  32619  suppss3  32654  iundisj2fi  32727  elrgspnsubrunlem1  33205  erlval  33216  lsmsnorb  33369  constrextdg2lem  33745  pstmfval  33893  ordtrest2NEW  33920  ldgenpisyslem1  34160  ldgenpisyslem2  34161  omsmeas  34321  sitgclbn  34341  eulerpartlemt  34369  eulerpartlemmf  34373  eulerpartlemgf  34377  bnj849  34922  bnj1136  34994  bnj1311  35021  bnj1413  35032  bnj1452  35049  blsconn  35238  cvmliftlem2  35280  cvmlift2lem12  35308  mvtss  35547  mthmpps  35576  ellcsrspsn  35635  neibastop2lem  36355  filnetlem3  36375  finxpsuclem  37392  poimirlem3  37624  mblfinlem3  37660  areacirclem2  37710  sdclem1  37744  istotbnd3  37772  sstotbnd  37776  iccbnd  37841  icccmpALT  37842  osumcllem1N  39957  osumcllem2N  39958  osumcllem4N  39960  osumcllem9N  39965  pexmidlem6N  39976  dihglblem3N  41296  dvhdimlem  41445  dochexmidlem6  41466  lcfrlem16  41559  lcfr  41586  aks6d1c6lem3  42167  rhmqusspan  42180  ssabdv  42215  hbtlem6  43125  iocinico  43208  oege2  43303  omabs2  43328  tfsconcatb0  43340  trclubgNEW  43614  cnvrcl0  43621  relexp0a  43712  brtrclfv2  43723  cotrclrcl  43738  frege77d  43742  unhe1  43781  ntrrn  44118  imo72b2lem2  44163  imo72b2  44168  mnuprdlem4  44271  radcnvrat  44310  iunconnlem2  44931  ssinss2d  45061  limccog  45625  limsupresico  45705  liminfresico  45776  icccncfext  45892  stoweidlem14  46019  fourierdlem20  46132  fourierdlem42  46154  fourierdlem46  46157  fourierdlem50  46161  fourierdlem51  46162  fourierdlem54  46165  fourierdlem64  46175  fourierdlem76  46187  fourierdlem102  46213  fourierdlem103  46214  fourierdlem104  46215  fourierdlem114  46225  meadjiunlem  46470  meaiininclem  46491  ovnsupge0  46562  hoidmvlelem2  46601  hoidmvlelem4  46603  vonvolmbllem  46665  vonvolmbl2  46668  vonvol2  46669  vonioolem1  46685  issmflem  46732  fsupdm  46847  finfdm  46851  fundcmpsurinjimaid  47416  perfectALTVlem2  47727  isubgruhgr  47872  uspgropssxp  48136  rhmsubcALTVlem4  48276  srhmsubcALTV  48317  imasubc  49144  imassc  49146  setrec2fun  49685  onsetreclem2  49699