Theorem eqsstrid 3969

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

Syntax hints:   → wi 4   = wceq 1541   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1781  df-cleq 2725  df-ss 3915

This theorem is referenced by:  eqsstrrid  3970  3sstr4g  3984  inss  4197  tpssi  4791  opabssxpd  5668  xpsspw  5755  fun  6693  fmpt  7052  fssrescdmd  7068  fliftrel  7251  knatar  7300  fr3nr  7714  ordsuci  7750  fiun  7884  f1iun  7885  1stcof  7960  2ndcof  7961  fsplitfpar  8057  fnwelem  8070  oeeui  8526  cofon1  8596  aceq3lem  10022  cflecard  10155  cfslb2n  10170  itunitc1  10322  axdc2lem  10350  axdc3lem2  10353  fpwwe2lem11  10543  canthwelem  10552  wuncval2  10649  peano5nni  12139  un0addcl  12425  un0mulcl  12426  fsuppmapnn0fiublem  13904  fsuppmapnn0fiub  13905  mertenslem2  15799  4sqlem11  16874  4sqlem19  16882  vdwlem13  16912  imasless  17452  rescfth  17854  oppchofcl  18174  oyoncl  18184  mgmidsssn0  18588  eqg0subg  19116  cycsubm  19122  efgsfo  19659  efgcpbllemb  19675  frgpuplem  19692  gsummpt1n0  19885  dprdfid  19939  dprd2d2  19966  ablfacrp  19988  ablfac1b  19992  ablfac1eu  19995  pgpfac1lem5  20001  ablfaclem3  20009  funcrngcsetc  20564  funcringcsetc  20598  srhmsubc  20604  rhmsubclem3  20611  lsptpcl  20921  lsppratlem3  21095  lsppratlem4  21096  lbsextlem2  21105  f1lindf  21768  topsn  22866  ordtbaslem  23123  ordtuni  23125  ordtbas2  23126  cnpco  23202  cnconst2  23218  tgcmp  23336  iunconn  23363  ptuni2  23511  xkococnlem  23594  tgqtop  23647  fbasrn  23819  uzrest  23832  fmco  23896  alexsubALT  23986  cnextf  24001  snclseqg  24051  ustund  24157  imasdsf1olem  24308  xmetresbl  24372  blsscls2  24439  metustss  24486  tngtopn  24585  reconn  24764  metnrmlem3  24797  cphsubrglem  25124  minveclem1  25371  minveclem3b  25375  ovolficcss  25417  ovolicc2lem4  25468  iundisj2  25497  uniioombllem4  25534  vitalilem5  25560  mbfeqalem1  25589  itg1addlem4  25647  limciun  25842  dvlip2  25947  dv11cn  25953  aalioulem3  26289  pserdvlem2  26385  pserdv  26386  abelthlem2  26389  efif1o  26502  efrlim  26926  efrlimOLD  26927  lgamgulmlem1  26986  fsumdvdsmul  27152  fsumdvdsmulOLD  27154  perfectlem2  27188  noextendseq  27626  nosupno  27662  nosupbnd2lem1  27674  noinfno  27677  noetasuplem4  27695  cuteq1  27798  bdayiun  27880  addsbday  27980  onscutlt  28221  onsiso  28225  bdayn0p1  28314  setsvtx  29034  uhgredgn0  29127  upgredgss  29131  umgredgss  29132  usgredgss  29158  umgrres1lem  29309  upgrres1  29312  1hegrvtxdg1r  29508  clwlknf1oclwwlknlem3  30084  minvecolem1  30875  sh0le  31441  mdslmd3i  32333  iundisj2f  32591  suppss2f  32642  2ndresdju  32653  fnpreimac  32675  fdifsuppconst  32694  suppss3  32730  iundisj2fi  32805  elrgspnsubrunlem1  33257  erlval  33268  lsmsnorb  33400  extvfvvcl  33628  extvfvcl  33629  esplyind  33659  esplyindfv  33660  esplyfvn  33661  constrextdg2lem  33833  pstmfval  33981  ordtrest2NEW  34008  ldgenpisyslem1  34248  ldgenpisyslem2  34249  omsmeas  34408  sitgclbn  34428  eulerpartlemt  34456  eulerpartlemmf  34460  eulerpartlemgf  34464  bnj849  35009  bnj1136  35081  bnj1311  35108  bnj1413  35119  bnj1452  35136  blsconn  35360  cvmliftlem2  35402  cvmlift2lem12  35430  mvtss  35669  mthmpps  35698  ellcsrspsn  35757  neibastop2lem  36476  filnetlem3  36496  finxpsuclem  37514  poimirlem3  37736  mblfinlem3  37772  areacirclem2  37822  sdclem1  37856  istotbnd3  37884  sstotbnd  37888  iccbnd  37953  icccmpALT  37954  osumcllem1N  40128  osumcllem2N  40129  osumcllem4N  40131  osumcllem9N  40136  pexmidlem6N  40147  dihglblem3N  41467  dvhdimlem  41616  dochexmidlem6  41637  lcfrlem16  41730  lcfr  41757  aks6d1c6lem3  42338  rhmqusspan  42351  ssabdv  42391  hbtlem6  43286  iocinico  43369  oege2  43464  omabs2  43489  tfsconcatb0  43501  trclubgNEW  43775  cnvrcl0  43782  relexp0a  43873  brtrclfv2  43884  cotrclrcl  43899  frege77d  43903  unhe1  43942  ntrrn  44279  imo72b2lem2  44324  imo72b2  44329  mnuprdlem4  44432  radcnvrat  44471  iunconnlem2  45091  ssinss2d  45221  limccog  45782  limsupresico  45860  liminfresico  45931  icccncfext  46047  stoweidlem14  46174  fourierdlem20  46287  fourierdlem42  46309  fourierdlem46  46312  fourierdlem50  46316  fourierdlem51  46317  fourierdlem54  46320  fourierdlem64  46330  fourierdlem76  46342  fourierdlem102  46368  fourierdlem103  46369  fourierdlem104  46370  fourierdlem114  46380  meadjiunlem  46625  meaiininclem  46646  ovnsupge0  46717  hoidmvlelem2  46756  hoidmvlelem4  46758  vonvolmbllem  46820  vonvolmbl2  46823  vonvol2  46824  vonioolem1  46840  preimageiingt  46880  issmflem  46887  fsupdm  47002  finfdm  47006  fundcmpsurinjimaid  47573  perfectALTVlem2  47884  isubgruhgr  48030  uspgropssxp  48306  rhmsubcALTVlem4  48446  srhmsubcALTV  48487  imasubc  49312  imassc  49314  setrec2fun  49853  onsetreclem2  49867