Theorem eqsstrid 4025

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

Syntax hints:   → wi 4   = wceq 1533   ⊆ wss 3944

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-9 2108  ax-ext 2696

This theorem depends on definitions:  df-bi 206  df-an 395  df-ex 1774  df-cleq 2717  df-ss 3961

This theorem is referenced by:  eqsstrrid  4026  inss  4237  tpssi  4841  opabssxpd  5725  xpsspw  5811  fun  6759  fmpt  7119  fssrescdmd  7135  fliftrel  7315  knatar  7364  fr3nr  7775  ordsuci  7812  sucexeloniOLD  7814  suceloniOLD  7816  fiun  7947  f1iun  7948  1stcof  8024  2ndcof  8025  fsplitfpar  8123  fnwelem  8136  oeeui  8623  cofon1  8693  aceq3lem  10145  cflecard  10278  cfslb2n  10293  itunitc1  10445  axdc3lem2  10476  fpwwe2lem11  10666  canthwelem  10675  wuncval2  10772  peano5nni  12248  un0addcl  12538  un0mulcl  12539  fsuppmapnn0fiublem  13991  fsuppmapnn0fiub  13992  mertenslem2  15867  4sqlem11  16927  4sqlem19  16935  vdwlem13  16965  imasless  17525  rescfth  17929  oppchofcl  18255  oyoncl  18265  mgmidsssn0  18635  eqg0subg  19159  cycsubm  19165  efgsfo  19706  efgcpbllemb  19722  frgpuplem  19739  gsummpt1n0  19932  dprdfid  19986  dprd2d2  20013  ablfacrp  20035  ablfac1b  20039  ablfac1eu  20042  pgpfac1lem5  20048  ablfaclem3  20056  funcrngcsetc  20585  funcringcsetc  20619  srhmsubc  20625  rhmsubclem3  20632  lsptpcl  20875  lsppratlem3  21049  lsppratlem4  21050  lbsextlem2  21059  f1lindf  21773  topsn  22877  ordtbaslem  23136  ordtuni  23138  ordtbas2  23139  cnpco  23215  cnconst2  23231  tgcmp  23349  iunconn  23376  ptuni2  23524  xkococnlem  23607  tgqtop  23660  fbasrn  23832  uzrest  23845  fmco  23909  alexsubALT  23999  cnextf  24014  snclseqg  24064  ustund  24170  imasdsf1olem  24323  xmetresbl  24387  blsscls2  24457  metustss  24504  tngtopn  24611  reconn  24788  metnrmlem3  24821  cphsubrglem  25149  minveclem1  25396  minveclem3b  25400  ovolficcss  25442  ovolicc2lem4  25493  iundisj2  25522  uniioombllem4  25559  vitalilem5  25585  mbfeqalem1  25614  itg1addlem4  25672  itg1addlem4OLD  25673  limciun  25867  dvlip2  25972  dv11cn  25978  aalioulem3  26314  pserdvlem2  26410  pserdv  26411  abelthlem2  26414  efif1o  26525  efrlim  26946  efrlimOLD  26947  lgamgulmlem1  27006  fsumdvdsmul  27172  fsumdvdsmulOLD  27174  perfectlem2  27208  noextendseq  27646  nosupno  27682  nosupbnd2lem1  27694  noinfno  27697  noetasuplem4  27715  cuteq1  27812  setsvtx  28920  uhgredgn0  29013  upgredgss  29017  umgredgss  29018  usgredgss  29044  umgrres1lem  29195  upgrres1  29198  1hegrvtxdg1r  29394  clwlknf1oclwwlknlem3  29965  minvecolem1  30756  sh0le  31322  mdslmd3i  32214  iundisj2f  32459  suppss2f  32505  2ndresdju  32516  fnpreimac  32538  fdifsuppconst  32551  suppss3  32588  iundisj2fi  32647  erlval  33048  lsmsnorb  33203  pstmfval  33628  ordtrest2NEW  33655  ldgenpisyslem1  33913  ldgenpisyslem2  33914  omsmeas  34074  sitgclbn  34094  eulerpartlemt  34122  eulerpartlemmf  34126  eulerpartlemgf  34130  bnj849  34687  bnj1136  34759  bnj1311  34786  bnj1413  34797  bnj1452  34814  blsconn  34985  cvmliftlem2  35027  cvmlift2lem12  35055  mvtss  35294  mthmpps  35323  neibastop2lem  35975  filnetlem3  35995  finxpsuclem  37007  poimirlem3  37227  mblfinlem3  37263  areacirclem2  37313  sdclem1  37347  istotbnd3  37375  sstotbnd  37379  iccbnd  37444  icccmpALT  37445  osumcllem1N  39559  osumcllem2N  39560  osumcllem4N  39562  osumcllem9N  39567  pexmidlem6N  39578  dihglblem3N  40898  dvhdimlem  41047  dochexmidlem6  41068  lcfrlem16  41161  lcfr  41188  aks6d1c6lem3  41775  rhmqusspan  41788  ssabdv  41842  hbtlem6  42695  iocinico  42782  oege2  42878  omabs2  42903  tfsconcatb0  42915  trclubgNEW  43190  cnvrcl0  43197  relexp0a  43288  brtrclfv2  43299  cotrclrcl  43314  frege77d  43318  unhe1  43357  ntrrn  43694  imo72b2lem0  43737  imo72b2lem2  43739  imo72b2  43744  mnuprdlem4  43854  radcnvrat  43893  iunconnlem2  44516  ssinss2d  44566  limccog  45146  limsupresico  45226  liminfresico  45297  icccncfext  45413  stoweidlem14  45540  fourierdlem20  45653  fourierdlem42  45675  fourierdlem46  45678  fourierdlem50  45682  fourierdlem51  45683  fourierdlem54  45686  fourierdlem64  45696  fourierdlem76  45708  fourierdlem102  45734  fourierdlem103  45735  fourierdlem104  45736  fourierdlem114  45746  meadjiunlem  45991  meaiininclem  46012  ovnsupge0  46083  hoidmvlelem2  46122  hoidmvlelem4  46124  vonvolmbllem  46186  vonvolmbl2  46189  vonvol2  46190  vonioolem1  46206  issmflem  46253  fsupdm  46368  finfdm  46372  fundcmpsurinjimaid  46888  perfectALTVlem2  47199  isubgruhgr  47338  uspgropssxp  47392  rhmsubcALTVlem4  47532  srhmsubcALTV  47573  setrec2fun  48309  onsetreclem2  48323