Theorem eqsstrid 3960

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2728  df-ss 3906

This theorem is referenced by:  eqsstrrid  3961  3sstr4g  3975  inss  4188  tpssi  4781  opabssxpd  5678  xpsspw  5765  fun  6702  fmpt  7062  fssrescdmd  7079  fliftrel  7263  knatar  7312  fr3nr  7726  ordsuci  7762  fiun  7896  f1iun  7897  1stcof  7972  2ndcof  7973  fsplitfpar  8068  fnwelem  8081  oeeui  8538  cofon1  8608  aceq3lem  10042  cflecard  10175  cfslb2n  10190  itunitc1  10342  axdc2lem  10370  axdc3lem2  10373  fpwwe2lem11  10564  canthwelem  10573  wuncval2  10670  peano5nni  12177  un0addcl  12470  un0mulcl  12471  fsuppmapnn0fiublem  13952  fsuppmapnn0fiub  13953  mertenslem2  15850  4sqlem11  16926  4sqlem19  16934  vdwlem13  16964  imasless  17504  rescfth  17906  oppchofcl  18226  oyoncl  18236  mgmidsssn0  18640  eqg0subg  19171  cycsubm  19177  efgsfo  19714  efgcpbllemb  19730  frgpuplem  19747  gsummpt1n0  19940  dprdfid  19994  dprd2d2  20021  ablfacrp  20043  ablfac1b  20047  ablfac1eu  20050  pgpfac1lem5  20056  ablfaclem3  20064  funcrngcsetc  20617  funcringcsetc  20651  srhmsubc  20657  rhmsubclem3  20664  lsptpcl  20974  lsppratlem3  21147  lsppratlem4  21148  lbsextlem2  21157  f1lindf  21802  topsn  22896  ordtbaslem  23153  ordtuni  23155  ordtbas2  23156  cnpco  23232  cnconst2  23248  tgcmp  23366  iunconn  23393  ptuni2  23541  xkococnlem  23624  tgqtop  23677  fbasrn  23849  uzrest  23862  fmco  23926  alexsubALT  24016  cnextf  24031  snclseqg  24081  ustund  24187  imasdsf1olem  24338  xmetresbl  24402  blsscls2  24469  metustss  24516  tngtopn  24615  reconn  24794  metnrmlem3  24827  cphsubrglem  25144  minveclem1  25391  minveclem3b  25395  ovolficcss  25436  ovolicc2lem4  25487  iundisj2  25516  uniioombllem4  25553  vitalilem5  25579  mbfeqalem1  25608  itg1addlem4  25666  limciun  25861  dvlip2  25962  dv11cn  25968  aalioulem3  26300  pserdvlem2  26393  pserdv  26394  abelthlem2  26397  efif1o  26510  efrlim  26933  lgamgulmlem1  26992  fsumdvdsmul  27158  perfectlem2  27193  noextendseq  27631  nosupno  27667  nosupbnd2lem1  27679  noinfno  27682  noetasuplem4  27700  cuteq1  27809  bdayiun  27907  addbday  28010  oncutlt  28256  oniso  28263  addonbday  28271  bdayn0p1  28361  bdaypw2n0bndlem  28455  setsvtx  29104  uhgredgn0  29197  upgredgss  29201  umgredgss  29202  usgredgss  29228  umgrres1lem  29379  upgrres1  29382  1hegrvtxdg1r  29577  clwlknf1oclwwlknlem3  30153  minvecolem1  30945  sh0le  31511  mdslmd3i  32403  iundisj2f  32660  suppss2f  32711  2ndresdju  32722  fnpreimac  32743  fdifsuppconst  32762  suppss3  32796  iundisj2fi  32870  elrgspnsubrunlem1  33308  erlval  33319  lsmsnorb  33451  extvfvvcl  33679  extvfvcl  33680  esplyind  33719  esplyindfv  33720  esplyfvn  33721  constrextdg2lem  33892  pstmfval  34040  ordtrest2NEW  34067  ldgenpisyslem1  34307  ldgenpisyslem2  34308  omsmeas  34467  sitgclbn  34487  eulerpartlemt  34515  eulerpartlemmf  34519  eulerpartlemgf  34523  bnj849  35067  bnj1136  35139  bnj1311  35166  bnj1413  35177  bnj1452  35194  blsconn  35426  cvmliftlem2  35468  cvmlift2lem12  35496  mvtss  35735  mthmpps  35764  ellcsrspsn  35823  neibastop2lem  36542  filnetlem3  36562  ttcmin  36678  finxpsuclem  37713  poimirlem3  37944  mblfinlem3  37980  areacirclem2  38030  sdclem1  38064  istotbnd3  38092  sstotbnd  38096  iccbnd  38161  icccmpALT  38162  osumcllem1N  40402  osumcllem2N  40403  osumcllem4N  40405  osumcllem9N  40410  pexmidlem6N  40421  dihglblem3N  41741  dvhdimlem  41890  dochexmidlem6  41911  lcfrlem16  42004  lcfr  42031  aks6d1c6lem3  42611  rhmqusspan  42624  ssabdv  42661  hbtlem6  43557  iocinico  43640  oege2  43735  omabs2  43760  tfsconcatb0  43772  trclubgNEW  44045  cnvrcl0  44052  relexp0a  44143  brtrclfv2  44154  cotrclrcl  44169  frege77d  44173  unhe1  44212  ntrrn  44549  imo72b2lem2  44594  imo72b2  44599  mnuprdlem4  44702  radcnvrat  44741  iunconnlem2  45361  ssinss2d  45491  limccog  46050  limsupresico  46128  liminfresico  46199  icccncfext  46315  stoweidlem14  46442  fourierdlem20  46555  fourierdlem42  46577  fourierdlem46  46580  fourierdlem50  46584  fourierdlem51  46585  fourierdlem54  46588  fourierdlem64  46598  fourierdlem76  46610  fourierdlem102  46636  fourierdlem103  46637  fourierdlem104  46638  fourierdlem114  46648  meadjiunlem  46893  meaiininclem  46914  ovnsupge0  46985  hoidmvlelem2  47024  hoidmvlelem4  47026  vonvolmbllem  47088  vonvolmbl2  47091  vonvol2  47092  vonioolem1  47108  preimageiingt  47148  issmflem  47155  fsupdm  47270  finfdm  47274  fundcmpsurinjimaid  47871  perfectALTVlem2  48198  isubgruhgr  48344  uspgropssxp  48620  rhmsubcALTVlem4  48760  srhmsubcALTV  48801  imasubc  49626  imassc  49628  setrec2fun  50167  onsetreclem2  50181