Theorem eqsstrid 3983

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

Syntax hints:   → wi 4   = wceq 1567   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1807  df-cleq 2761  df-ss 3930

This theorem is referenced by:  eqsstrrid  3984  3sstr4g  3998  inss  4209  tpssi  4804  opabssxpd  5706  xpsspw  5794  fun  6738  fmpt  7103  fssrescdmd  7120  fliftrel  7304  knatar  7353  fr3nr  7767  ordsuci  7803  fiun  7936  f1iun  7937  1stcof  8012  2ndcof  8013  fsplitfpar  8109  fnwelem  8123  oeeui  8584  cofon1  8654  aceq3lem  10100  cflecard  10232  cfslb2n  10248  itunitc1  10400  axdc2lem  10428  axdc3lem2  10431  fpwwe2lem11  10622  canthwelem  10631  wuncval2  10728  peano5nni  12232  un0addcl  12533  un0mulcl  12534  fsuppmapnn0fiublem  14022  fsuppmapnn0fiub  14023  mertenslem2  15935  4sqlem11  17011  4sqlem19  17019  vdwlem13  17049  imasless  17590  rescfth  17992  oppchofcl  18312  oyoncl  18322  mgmidsssn0  18726  eqg0subg  19263  cycsubm  19269  efgsfo  19805  efgcpbllemb  19821  frgpuplem  19838  gsummpt1n0  20031  dprdfid  20085  dprd2d2  20112  ablfacrp  20134  ablfac1b  20138  ablfac1eu  20141  pgpfac1lem5  20147  ablfaclem3  20155  funcrngcsetc  20721  funcringcsetc  20755  srhmsubc  20761  rhmsubclem3  20768  lsptpcl  21074  lsppratlem3  21247  lsppratlem4  21248  lbsextlem2  21257  f1lindf  21937  topsn  23053  ordtbaslem  23310  ordtuni  23312  ordtbas2  23313  cnpco  23389  cnconst2  23405  tgcmp  23523  iunconn  23550  ptuni2  23698  xkococnlem  23781  tgqtop  23834  fbasrn  24006  uzrest  24019  fmco  24083  alexsubALT  24173  cnextf  24188  snclseqg  24238  ustund  24344  imasdsf1olem  24495  xmetresbl  24559  blsscls2  24626  metustss  24673  tngtopn  24772  reconn  24951  metnrmlem3  24984  cphsubrglem  25301  minveclem1  25548  minveclem3b  25552  ovolficcss  25593  ovolicc2lem4  25644  iundisj2  25673  uniioombllem4  25710  vitalilem5  25736  mbfeqalem1  25765  itg1addlem4  25823  limciun  26018  dvlip2  26119  dv11cn  26125  aalioulem3  26460  pserdvlem2  26553  pserdv  26554  abelthlem2  26557  efif1o  26673  efrlim  27096  lgamgulmlem1  27155  fsumdvdsmul  27321  perfectlem2  27356  noextendseq  27793  nosupno  27829  nosupbnd2lem1  27841  noinfno  27844  noetasuplem4  27862  cuteq1  27972  bdayiun  28070  addbday  28173  oncutlt  28419  oniso  28426  addonbday  28434  bdayn0p1  28524  bdaypw2n0bndlem  28618  setsvtx  29322  uhgredgn0  29415  upgredgss  29419  umgredgss  29420  usgredgss  29446  umgrres1lem  29597  upgrres1  29600  1hegrvtxdg1r  29795  clwlknf1oclwwlknlem3  30371  minvecolem1  31163  sh0le  31729  mdslmd3i  32621  iundisj2f  32872  suppss2f  32920  2ndresdju  32931  fnpreimac  32952  fdifsuppconst  32971  suppss3  33005  iundisj2fi  33079  elrgspnsubrunlem1  33504  erlval  33515  lsmsnorb  33644  extvfvvcl  33866  extvfvcl  33867  esplyind  33906  esplyindfv  33907  esplyfvn  33908  constrextdg2lem  34079  pstmfval  34227  ordtrest2NEW  34254  ldgenpisyslem1  34494  ldgenpisyslem2  34495  omsmeas  34654  sitgclbn  34674  eulerpartlemt  34702  eulerpartlemmf  34706  eulerpartlemgf  34710  bnj849  35254  bnj1136  35326  bnj1311  35353  bnj1413  35364  bnj1452  35381  vonf1oonfo  35494  blsconn  35631  cvmliftlem2  35673  cvmlift2lem12  35701  mvtss  35940  mthmpps  35969  ellcsrspsn  36028  neibastop2lem  36756  filnetlem3  36776  ttcmin  36892  finxpsuclem  37926  poimirlem3  38157  mblfinlem3  38193  areacirclem2  38243  sdclem1  38277  istotbnd3  38305  sstotbnd  38309  iccbnd  38374  icccmpALT  38375  osumcllem1N  40615  osumcllem2N  40616  osumcllem4N  40618  osumcllem9N  40623  pexmidlem6N  40634  dihglblem3N  41954  dvhdimlem  42103  dochexmidlem6  42124  lcfrlem16  42217  lcfr  42244  aks6d1c6lem3  42824  rhmqusspan  42837  ssabdv  42874  hbtlem6  43741  iocinico  43824  oege2  43919  omabs2  43944  tfsconcatb0  43956  trclubgNEW  44229  cnvrcl0  44236  relexp0a  44327  brtrclfv2  44338  cotrclrcl  44353  frege77d  44357  unhe1  44396  ntrrn  44733  imo72b2lem2  44778  imo72b2  44783  mnuprdlem4  44870  radcnvrat  44909  iunconnlem2  45528  ssinss2d  45665  limccog  46221  limsupresico  46299  liminfresico  46370  icccncfext  46486  stoweidlem14  46613  fourierdlem20  46726  fourierdlem42  46748  fourierdlem46  46751  fourierdlem50  46755  fourierdlem51  46756  fourierdlem54  46759  fourierdlem64  46769  fourierdlem76  46781  fourierdlem102  46807  fourierdlem103  46808  fourierdlem104  46809  fourierdlem114  46819  meadjiunlem  47064  meaiininclem  47085  ovnsupge0  47156  hoidmvlelem2  47195  hoidmvlelem4  47197  vonvolmbllem  47259  vonvolmbl2  47262  vonvol2  47263  vonioolem1  47279  preimageiingt  47319  issmflem  47326  fsupdm  47441  finfdm  47445  fundcmpsurinjimaid  48042  perfectALTVlem2  48369  isubgruhgr  48515  uspgropssxp  48791  rhmsubcALTVlem4  48931  srhmsubcALTV  48972  imasubc  49807  imassc  49809  setrec2fun  50348  onsetreclem2  50362