Theorem eqsstrid 3968

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

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

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 2121  ax-ext 2703

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

This theorem is referenced by:  eqsstrrid  3969  3sstr4g  3983  inss  4193  tpssi  4785  opabssxpd  5658  xpsspw  5744  fun  6680  fmpt  7038  fssrescdmd  7054  fliftrel  7237  knatar  7286  fr3nr  7700  ordsuci  7736  fiun  7870  f1iun  7871  1stcof  7946  2ndcof  7947  fsplitfpar  8043  fnwelem  8056  oeeui  8512  cofon1  8582  aceq3lem  10006  cflecard  10139  cfslb2n  10154  itunitc1  10306  axdc3lem2  10337  fpwwe2lem11  10527  canthwelem  10536  wuncval2  10633  peano5nni  12123  un0addcl  12409  un0mulcl  12410  fsuppmapnn0fiublem  13892  fsuppmapnn0fiub  13893  mertenslem2  15787  4sqlem11  16862  4sqlem19  16870  vdwlem13  16900  imasless  17439  rescfth  17841  oppchofcl  18161  oyoncl  18171  mgmidsssn0  18575  eqg0subg  19103  cycsubm  19109  efgsfo  19646  efgcpbllemb  19662  frgpuplem  19679  gsummpt1n0  19872  dprdfid  19926  dprd2d2  19953  ablfacrp  19975  ablfac1b  19979  ablfac1eu  19982  pgpfac1lem5  19988  ablfaclem3  19996  funcrngcsetc  20550  funcringcsetc  20584  srhmsubc  20590  rhmsubclem3  20597  lsptpcl  20907  lsppratlem3  21081  lsppratlem4  21082  lbsextlem2  21091  f1lindf  21754  topsn  22841  ordtbaslem  23098  ordtuni  23100  ordtbas2  23101  cnpco  23177  cnconst2  23193  tgcmp  23311  iunconn  23338  ptuni2  23486  xkococnlem  23569  tgqtop  23622  fbasrn  23794  uzrest  23807  fmco  23871  alexsubALT  23961  cnextf  23976  snclseqg  24026  ustund  24132  imasdsf1olem  24283  xmetresbl  24347  blsscls2  24414  metustss  24461  tngtopn  24560  reconn  24739  metnrmlem3  24772  cphsubrglem  25099  minveclem1  25346  minveclem3b  25350  ovolficcss  25392  ovolicc2lem4  25443  iundisj2  25472  uniioombllem4  25509  vitalilem5  25535  mbfeqalem1  25564  itg1addlem4  25622  limciun  25817  dvlip2  25922  dv11cn  25928  aalioulem3  26264  pserdvlem2  26360  pserdv  26361  abelthlem2  26364  efif1o  26477  efrlim  26901  efrlimOLD  26902  lgamgulmlem1  26961  fsumdvdsmul  27127  fsumdvdsmulOLD  27129  perfectlem2  27163  noextendseq  27601  nosupno  27637  nosupbnd2lem1  27649  noinfno  27652  noetasuplem4  27670  cuteq1  27773  bdayiun  27855  addsbday  27955  onscutlt  28196  onsiso  28200  bdayn0p1  28289  setsvtx  29008  uhgredgn0  29101  upgredgss  29105  umgredgss  29106  usgredgss  29132  umgrres1lem  29283  upgrres1  29286  1hegrvtxdg1r  29482  clwlknf1oclwwlknlem3  30055  minvecolem1  30846  sh0le  31412  mdslmd3i  32304  iundisj2f  32562  suppss2f  32612  2ndresdju  32623  fnpreimac  32645  fdifsuppconst  32662  suppss3  32698  iundisj2fi  32771  elrgspnsubrunlem1  33206  erlval  33217  lsmsnorb  33348  constrextdg2lem  33753  pstmfval  33901  ordtrest2NEW  33928  ldgenpisyslem1  34168  ldgenpisyslem2  34169  omsmeas  34328  sitgclbn  34348  eulerpartlemt  34376  eulerpartlemmf  34380  eulerpartlemgf  34384  bnj849  34929  bnj1136  35001  bnj1311  35028  bnj1413  35039  bnj1452  35056  blsconn  35280  cvmliftlem2  35322  cvmlift2lem12  35350  mvtss  35589  mthmpps  35618  ellcsrspsn  35677  neibastop2lem  36394  filnetlem3  36414  finxpsuclem  37431  poimirlem3  37663  mblfinlem3  37699  areacirclem2  37749  sdclem1  37783  istotbnd3  37811  sstotbnd  37815  iccbnd  37880  icccmpALT  37881  osumcllem1N  39995  osumcllem2N  39996  osumcllem4N  39998  osumcllem9N  40003  pexmidlem6N  40014  dihglblem3N  41334  dvhdimlem  41483  dochexmidlem6  41504  lcfrlem16  41597  lcfr  41624  aks6d1c6lem3  42205  rhmqusspan  42218  ssabdv  42253  hbtlem6  43162  iocinico  43245  oege2  43340  omabs2  43365  tfsconcatb0  43377  trclubgNEW  43651  cnvrcl0  43658  relexp0a  43749  brtrclfv2  43760  cotrclrcl  43775  frege77d  43779  unhe1  43818  ntrrn  44155  imo72b2lem2  44200  imo72b2  44205  mnuprdlem4  44308  radcnvrat  44347  iunconnlem2  44967  ssinss2d  45097  limccog  45660  limsupresico  45738  liminfresico  45809  icccncfext  45925  stoweidlem14  46052  fourierdlem20  46165  fourierdlem42  46187  fourierdlem46  46190  fourierdlem50  46194  fourierdlem51  46195  fourierdlem54  46198  fourierdlem64  46208  fourierdlem76  46220  fourierdlem102  46246  fourierdlem103  46247  fourierdlem104  46248  fourierdlem114  46258  meadjiunlem  46503  meaiininclem  46524  ovnsupge0  46595  hoidmvlelem2  46634  hoidmvlelem4  46636  vonvolmbllem  46698  vonvolmbl2  46701  vonvol2  46702  vonioolem1  46718  issmflem  46765  fsupdm  46880  finfdm  46884  fundcmpsurinjimaid  47442  perfectALTVlem2  47753  isubgruhgr  47899  uspgropssxp  48175  rhmsubcALTVlem4  48315  srhmsubcALTV  48356  imasubc  49183  imassc  49185  setrec2fun  49724  onsetreclem2  49738