Theorem eqsstrid 4002

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3931

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1779  df-cleq 2726  df-ss 3948

This theorem is referenced by:  eqsstrrid  4003  3sstr4g  4017  inss  4228  tpssi  4818  opabssxpd  5712  xpsspw  5799  fun  6750  fmpt  7110  fssrescdmd  7126  fliftrel  7310  knatar  7359  fr3nr  7774  ordsuci  7810  sucexeloniOLD  7812  suceloniOLD  7814  fiun  7949  f1iun  7950  1stcof  8026  2ndcof  8027  fsplitfpar  8125  fnwelem  8138  oeeui  8622  cofon1  8692  aceq3lem  10142  cflecard  10275  cfslb2n  10290  itunitc1  10442  axdc3lem2  10473  fpwwe2lem11  10663  canthwelem  10672  wuncval2  10769  peano5nni  12251  un0addcl  12542  un0mulcl  12543  fsuppmapnn0fiublem  14013  fsuppmapnn0fiub  14014  mertenslem2  15903  4sqlem11  16975  4sqlem19  16983  vdwlem13  17013  imasless  17556  rescfth  17955  oppchofcl  18275  oyoncl  18285  mgmidsssn0  18654  eqg0subg  19183  cycsubm  19189  efgsfo  19725  efgcpbllemb  19741  frgpuplem  19758  gsummpt1n0  19951  dprdfid  20005  dprd2d2  20032  ablfacrp  20054  ablfac1b  20058  ablfac1eu  20061  pgpfac1lem5  20067  ablfaclem3  20075  funcrngcsetc  20608  funcringcsetc  20642  srhmsubc  20648  rhmsubclem3  20655  lsptpcl  20945  lsppratlem3  21119  lsppratlem4  21120  lbsextlem2  21129  f1lindf  21796  topsn  22885  ordtbaslem  23142  ordtuni  23144  ordtbas2  23145  cnpco  23221  cnconst2  23237  tgcmp  23355  iunconn  23382  ptuni2  23530  xkococnlem  23613  tgqtop  23666  fbasrn  23838  uzrest  23851  fmco  23915  alexsubALT  24005  cnextf  24020  snclseqg  24070  ustund  24176  imasdsf1olem  24328  xmetresbl  24392  blsscls2  24461  metustss  24508  tngtopn  24607  reconn  24786  metnrmlem3  24819  cphsubrglem  25147  minveclem1  25394  minveclem3b  25398  ovolficcss  25440  ovolicc2lem4  25491  iundisj2  25520  uniioombllem4  25557  vitalilem5  25583  mbfeqalem1  25612  itg1addlem4  25670  limciun  25865  dvlip2  25970  dv11cn  25976  aalioulem3  26312  pserdvlem2  26408  pserdv  26409  abelthlem2  26412  efif1o  26524  efrlim  26948  efrlimOLD  26949  lgamgulmlem1  27008  fsumdvdsmul  27174  fsumdvdsmulOLD  27176  perfectlem2  27210  noextendseq  27648  nosupno  27684  nosupbnd2lem1  27696  noinfno  27699  noetasuplem4  27717  cuteq1  27814  addsbday  27986  setsvtx  28980  uhgredgn0  29073  upgredgss  29077  umgredgss  29078  usgredgss  29104  umgrres1lem  29255  upgrres1  29258  1hegrvtxdg1r  29454  clwlknf1oclwwlknlem3  30030  minvecolem1  30821  sh0le  31387  mdslmd3i  32279  iundisj2f  32538  suppss2f  32583  2ndresdju  32594  fnpreimac  32616  fdifsuppconst  32633  suppss3  32670  iundisj2fi  32738  elrgspnsubrunlem1  33190  erlval  33201  lsmsnorb  33354  constrextdg2lem  33728  pstmfval  33854  ordtrest2NEW  33881  ldgenpisyslem1  34123  ldgenpisyslem2  34124  omsmeas  34284  sitgclbn  34304  eulerpartlemt  34332  eulerpartlemmf  34336  eulerpartlemgf  34340  bnj849  34898  bnj1136  34970  bnj1311  34997  bnj1413  35008  bnj1452  35025  blsconn  35208  cvmliftlem2  35250  cvmlift2lem12  35278  mvtss  35517  mthmpps  35546  ellcsrspsn  35605  neibastop2lem  36320  filnetlem3  36340  finxpsuclem  37357  poimirlem3  37589  mblfinlem3  37625  areacirclem2  37675  sdclem1  37709  istotbnd3  37737  sstotbnd  37741  iccbnd  37806  icccmpALT  37807  osumcllem1N  39917  osumcllem2N  39918  osumcllem4N  39920  osumcllem9N  39925  pexmidlem6N  39936  dihglblem3N  41256  dvhdimlem  41405  dochexmidlem6  41426  lcfrlem16  41519  lcfr  41546  aks6d1c6lem3  42132  rhmqusspan  42145  ssabdv  42218  hbtlem6  43104  iocinico  43187  oege2  43282  omabs2  43307  tfsconcatb0  43319  trclubgNEW  43593  cnvrcl0  43600  relexp0a  43691  brtrclfv2  43702  cotrclrcl  43717  frege77d  43721  unhe1  43760  ntrrn  44097  imo72b2lem2  44142  imo72b2  44147  mnuprdlem4  44251  radcnvrat  44290  iunconnlem2  44912  ssinss2d  45022  limccog  45592  limsupresico  45672  liminfresico  45743  icccncfext  45859  stoweidlem14  45986  fourierdlem20  46099  fourierdlem42  46121  fourierdlem46  46124  fourierdlem50  46128  fourierdlem51  46129  fourierdlem54  46132  fourierdlem64  46142  fourierdlem76  46154  fourierdlem102  46180  fourierdlem103  46181  fourierdlem104  46182  fourierdlem114  46192  meadjiunlem  46437  meaiininclem  46458  ovnsupge0  46529  hoidmvlelem2  46568  hoidmvlelem4  46570  vonvolmbllem  46632  vonvolmbl2  46635  vonvol2  46636  vonioolem1  46652  issmflem  46699  fsupdm  46814  finfdm  46818  fundcmpsurinjimaid  47356  perfectALTVlem2  47667  isubgruhgr  47812  uspgropssxp  48018  rhmsubcALTVlem4  48158  srhmsubcALTV  48199  setrec2fun  49219  onsetreclem2  49233