Theorem eqsstrid 3972

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

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

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 2708

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

This theorem is referenced by:  eqsstrrid  3973  3sstr4g  3987  inss  4200  tpssi  4794  opabssxpd  5671  xpsspw  5758  fun  6696  fmpt  7055  fssrescdmd  7071  fliftrel  7254  knatar  7303  fr3nr  7717  ordsuci  7753  fiun  7887  f1iun  7888  1stcof  7963  2ndcof  7964  fsplitfpar  8060  fnwelem  8073  oeeui  8530  cofon1  8600  aceq3lem  10030  cflecard  10163  cfslb2n  10178  itunitc1  10330  axdc2lem  10358  axdc3lem2  10361  fpwwe2lem11  10552  canthwelem  10561  wuncval2  10658  peano5nni  12148  un0addcl  12434  un0mulcl  12435  fsuppmapnn0fiublem  13913  fsuppmapnn0fiub  13914  mertenslem2  15808  4sqlem11  16883  4sqlem19  16891  vdwlem13  16921  imasless  17461  rescfth  17863  oppchofcl  18183  oyoncl  18193  mgmidsssn0  18597  eqg0subg  19125  cycsubm  19131  efgsfo  19668  efgcpbllemb  19684  frgpuplem  19701  gsummpt1n0  19894  dprdfid  19948  dprd2d2  19975  ablfacrp  19997  ablfac1b  20001  ablfac1eu  20004  pgpfac1lem5  20010  ablfaclem3  20018  funcrngcsetc  20573  funcringcsetc  20607  srhmsubc  20613  rhmsubclem3  20620  lsptpcl  20930  lsppratlem3  21104  lsppratlem4  21105  lbsextlem2  21114  f1lindf  21777  topsn  22875  ordtbaslem  23132  ordtuni  23134  ordtbas2  23135  cnpco  23211  cnconst2  23227  tgcmp  23345  iunconn  23372  ptuni2  23520  xkococnlem  23603  tgqtop  23656  fbasrn  23828  uzrest  23841  fmco  23905  alexsubALT  23995  cnextf  24010  snclseqg  24060  ustund  24166  imasdsf1olem  24317  xmetresbl  24381  blsscls2  24448  metustss  24495  tngtopn  24594  reconn  24773  metnrmlem3  24806  cphsubrglem  25133  minveclem1  25380  minveclem3b  25384  ovolficcss  25426  ovolicc2lem4  25477  iundisj2  25506  uniioombllem4  25543  vitalilem5  25569  mbfeqalem1  25598  itg1addlem4  25656  limciun  25851  dvlip2  25956  dv11cn  25962  aalioulem3  26298  pserdvlem2  26394  pserdv  26395  abelthlem2  26398  efif1o  26511  efrlim  26935  efrlimOLD  26936  lgamgulmlem1  26995  fsumdvdsmul  27161  fsumdvdsmulOLD  27163  perfectlem2  27197  noextendseq  27635  nosupno  27671  nosupbnd2lem1  27683  noinfno  27686  noetasuplem4  27704  cuteq1  27813  bdayiun  27911  addbday  28014  oncutlt  28260  oniso  28267  addonbday  28275  bdayn0p1  28365  bdaypw2n0bndlem  28459  setsvtx  29108  uhgredgn0  29201  upgredgss  29205  umgredgss  29206  usgredgss  29232  umgrres1lem  29383  upgrres1  29386  1hegrvtxdg1r  29582  clwlknf1oclwwlknlem3  30158  minvecolem1  30949  sh0le  31515  mdslmd3i  32407  iundisj2f  32665  suppss2f  32716  2ndresdju  32727  fnpreimac  32749  fdifsuppconst  32768  suppss3  32802  iundisj2fi  32877  elrgspnsubrunlem1  33329  erlval  33340  lsmsnorb  33472  extvfvvcl  33700  extvfvcl  33701  esplyind  33731  esplyindfv  33732  esplyfvn  33733  constrextdg2lem  33905  pstmfval  34053  ordtrest2NEW  34080  ldgenpisyslem1  34320  ldgenpisyslem2  34321  omsmeas  34480  sitgclbn  34500  eulerpartlemt  34528  eulerpartlemmf  34532  eulerpartlemgf  34536  bnj849  35081  bnj1136  35153  bnj1311  35180  bnj1413  35191  bnj1452  35208  blsconn  35438  cvmliftlem2  35480  cvmlift2lem12  35508  mvtss  35747  mthmpps  35776  ellcsrspsn  35835  neibastop2lem  36554  filnetlem3  36574  finxpsuclem  37602  poimirlem3  37824  mblfinlem3  37860  areacirclem2  37910  sdclem1  37944  istotbnd3  37972  sstotbnd  37976  iccbnd  38041  icccmpALT  38042  osumcllem1N  40216  osumcllem2N  40217  osumcllem4N  40219  osumcllem9N  40224  pexmidlem6N  40235  dihglblem3N  41555  dvhdimlem  41704  dochexmidlem6  41725  lcfrlem16  41818  lcfr  41845  aks6d1c6lem3  42426  rhmqusspan  42439  ssabdv  42476  hbtlem6  43371  iocinico  43454  oege2  43549  omabs2  43574  tfsconcatb0  43586  trclubgNEW  43859  cnvrcl0  43866  relexp0a  43957  brtrclfv2  43968  cotrclrcl  43983  frege77d  43987  unhe1  44026  ntrrn  44363  imo72b2lem2  44408  imo72b2  44413  mnuprdlem4  44516  radcnvrat  44555  iunconnlem2  45175  ssinss2d  45305  limccog  45866  limsupresico  45944  liminfresico  46015  icccncfext  46131  stoweidlem14  46258  fourierdlem20  46371  fourierdlem42  46393  fourierdlem46  46396  fourierdlem50  46400  fourierdlem51  46401  fourierdlem54  46404  fourierdlem64  46414  fourierdlem76  46426  fourierdlem102  46452  fourierdlem103  46453  fourierdlem104  46454  fourierdlem114  46464  meadjiunlem  46709  meaiininclem  46730  ovnsupge0  46801  hoidmvlelem2  46840  hoidmvlelem4  46842  vonvolmbllem  46904  vonvolmbl2  46907  vonvol2  46908  vonioolem1  46924  preimageiingt  46964  issmflem  46971  fsupdm  47086  finfdm  47090  fundcmpsurinjimaid  47657  perfectALTVlem2  47968  isubgruhgr  48114  uspgropssxp  48390  rhmsubcALTVlem4  48530  srhmsubcALTV  48571  imasubc  49396  imassc  49398  setrec2fun  49937  onsetreclem2  49951