Theorem eqsstrid 3951

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3900

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2755  df-ss 3901

This theorem is used by:  eqsstrrid  3952  3sstr4g  3966  inss  4148  tpssi  4796  opabssxpd  5703  xpsspw  5794  fun  6772  fmpt  7140  fssrescdmd  7157  fliftrel  7345  knatar  7396  fr3nr  7816  ordsuci  7854  fiun  7987  f1iun  7988  1stcof  8063  2ndcof  8064  fsplitfpar  8164  fnwelem  8178  oeeui  8647  cofon1  8717  setrec2fun  10008  aceq3lem  10236  cflecard  10367  cfslb2n  10383  itunitc1  10535  axdc2lem  10563  axdc3lem2  10566  fpwwe2lem11  10763  canthwelem  10772  wuncval2  10869  peano5nni  12376  un0addcl  12677  un0mulcl  12678  fsuppmapnn0fiublem  14171  fsuppmapnn0fiub  14172  mertenslem2  16095  4sqlem11  17174  4sqlem19  17182  vdwlem13  17212  imasless  17753  rescfth  18155  oppchofcl  18475  oyoncl  18485  mgmidsssn0  18894  eqg0subg  19452  cycsubm  19458  efgsfo  19995  efgcpbllemb  20011  frgpuplem  20028  gsummpt1n0  20221  dprdfid  20275  dprd2d2  20302  ablfacrp  20324  ablfac1b  20328  ablfac1eu  20331  pgpfac1lem5  20337  ablfaclem3  20345  funcrngcsetc  20934  funcringcsetc  20968  srhmsubc  20974  rhmsubclem3  20981  lsptpcl  21296  lsppratlem3  21469  lsppratlem4  21470  lbsextlem2  21479  f1lindf  22172  topsn  23293  ordtbaslem  23550  ordtuni  23552  ordtbas2  23553  cnpco  23629  cnconst2  23645  tgcmp  23763  iunconn  23790  ptuni2  23939  xkococnlem  24022  tgqtop  24075  fbasrn  24247  uzrest  24260  fmco  24324  alexsubALT  24414  cnextf  24429  snclseqg  24479  ustund  24585  imasdsf1olem  24736  xmetresbl  24800  blsscls2  24867  metustss  24914  tngtopn  25013  reconn  25192  metnrmlem3  25225  cphsubrglem  25542  minveclem1  25789  minveclem3b  25793  ovolficcss  25834  ovolicc2lem4  25885  iundisj2  25914  uniioombllem4  25951  vitalilem5  25977  mbfeqalem1  26006  itg1addlem4  26064  limciun  26258  dvlip2  26359  dv11cn  26365  aalioulem3  26707  pserdvlem2  26801  pserdv  26802  abelthlem2  26805  efif1o  26920  efrlim  27343  lgamgulmlem1  27402  fsumdvdsmul  27568  perfectlem2  27603  noextendseq  28070  nosupno  28106  nosupbnd2lem1  28118  noinfno  28121  noetasuplem4  28139  cuteq1  28249  bdayiun  28347  addbday  28450  oncutlt  28696  oniso  28703  addonbday  28711  bdayn0p1  28801  bdaypw2n0bndlem  28895  setsvtx  29659  uhgredgn0  29752  upgredgss  29756  umgredgss  29757  usgredgss  29786  umgrres1lem  29937  upgrres1  29940  1hegrvtxdg1r  30135  clwlknf1oclwwlknlem3  30720  minvecolem1  31522  sh0le  32088  mdslmd3i  32980  iundisj2f  33272  suppss2f  33320  2ndresdju  33331  fnpreimac  33352  fdifsuppconst  33369  suppss3  33401  iundisj2fi  33475  elrgspnsubrunlem1  33897  erlval  33908  lsmsnorb  34043  extvfvvcl  34271  extvfvcl  34272  esplyind  34311  esplyindfv  34312  esplyfvn  34313  constrextdg2lem  34484  pstmfval  34632  ordtrest2NEW  34659  ldgenpisyslem1  34900  ldgenpisyslem2  34901  omsmeas  35059  sitgclbn  35079  eulerpartlemt  35107  eulerpartlemmf  35111  eulerpartlemgf  35115  bnj849  35659  bnj1136  35731  bnj1311  35758  bnj1413  35769  bnj1452  35786  kardnnfi  35971  rankkardu  35973  vonf1oonfo  36083  blsconn  36210  cvmliftlem2  36252  cvmlift2lem12  36280  mvtss  36519  mthmpps  36548  ellcsrspsn  36607  neibastop2lem  37356  filnetlem3  37376  ttcmin  37492  coindir  38210  cossidres2  38214  cossidcnvss2  38215  cossidcnvss  38216  finxpsuclem  38581  poimirlem3  38802  mblfinlem3  38838  areacirclem2  38888  dfprop2  38907  sdclem1  38936  istotbnd3  38964  sstotbnd  38968  iccbnd  39033  icccmpALT  39034  osumcllem1N  41272  osumcllem2N  41273  osumcllem4N  41275  osumcllem9N  41280  pexmidlem6N  41291  dihglblem3N  42611  dvhdimlem  42760  dochexmidlem6  42781  lcfrlem16  42874  lcfr  42901  aks6d1c6lem3  43481  rhmqusspan  43494  ssabdv  43534  hbtlem6  44390  iocinico  44469  oege2  44564  omabs2  44589  tfsconcatb0  44601  trclubgNEW  44873  cnvrcl0  44880  relexp0a  44971  brtrclfv2  44982  cotrclrcl  44997  frege77d  45001  unhe1  45040  ntrrn  45377  imo72b2lem2  45422  imo72b2  45427  mnuprdlem4  45514  radcnvrat  45553  iunconnlem2  46171  grpcanonhfstruct  46293  ssinss2d  46345  limccog  46899  limsupresico  46977  liminfresico  47048  icccncfext  47164  stoweidlem14  47291  fourierdlem20  47404  fourierdlem42  47426  fourierdlem46  47429  fourierdlem50  47433  fourierdlem51  47434  fourierdlem54  47437  fourierdlem64  47447  fourierdlem76  47459  fourierdlem102  47485  fourierdlem103  47486  fourierdlem104  47487  fourierdlem114  47497  meadjiunlem  47742  meaiininclem  47763  ovnsupge0  47834  hoidmvlelem2  47873  hoidmvlelem4  47875  vonvolmbllem  47937  vonvolmbl2  47940  vonvol2  47941  vonioolem1  47957  preimageiingt  47997  issmflem  48004  fsupdm  48119  finfdm  48123  fundcmpsurinjimaid  48760  perfectALTVlem2  49087  isubgruhgr  49233  uspgropssxp  49509  rhmsubcALTVlem4  49648  srhmsubcALTV  49689  imasubc  50592  imassc  50594  onsetreclem2  51199