Theorem eqsstrid 3969

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

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

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 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2733

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

This theorem is used by:  eqsstrrid  3970  3sstr4g  3984  inss  4194  tpssi  4798  opabssxpd  5698  xpsspw  5787  fun  6742  fmpt  7108  fssrescdmd  7125  fliftrel  7314  knatar  7365  fr3nr  7784  ordsuci  7820  fiun  7953  f1iun  7954  1stcof  8029  2ndcof  8030  fsplitfpar  8127  fnwelem  8141  oeeui  8604  cofon1  8674  setrec2fun  9966  aceq3lem  10192  cflecard  10323  cfslb2n  10339  itunitc1  10491  axdc2lem  10519  axdc3lem2  10522  fpwwe2lem11  10719  canthwelem  10728  wuncval2  10825  peano5nni  12331  un0addcl  12632  un0mulcl  12633  fsuppmapnn0fiublem  14126  fsuppmapnn0fiub  14127  mertenslem2  16047  4sqlem11  17126  4sqlem19  17134  vdwlem13  17164  imasless  17705  rescfth  18107  oppchofcl  18427  oyoncl  18437  mgmidsssn0  18846  eqg0subg  19404  cycsubm  19410  efgsfo  19946  efgcpbllemb  19962  frgpuplem  19979  gsummpt1n0  20172  dprdfid  20226  dprd2d2  20253  ablfacrp  20275  ablfac1b  20279  ablfac1eu  20282  pgpfac1lem5  20288  ablfaclem3  20296  funcrngcsetc  20885  funcringcsetc  20919  srhmsubc  20925  rhmsubclem3  20932  lsptpcl  21247  lsppratlem3  21420  lsppratlem4  21421  lbsextlem2  21430  f1lindf  22121  topsn  23242  ordtbaslem  23499  ordtuni  23501  ordtbas2  23502  cnpco  23578  cnconst2  23594  tgcmp  23712  iunconn  23739  ptuni2  23888  xkococnlem  23971  tgqtop  24024  fbasrn  24196  uzrest  24209  fmco  24273  alexsubALT  24363  cnextf  24378  snclseqg  24428  ustund  24534  imasdsf1olem  24685  xmetresbl  24749  blsscls2  24816  metustss  24863  tngtopn  24962  reconn  25141  metnrmlem3  25174  cphsubrglem  25491  minveclem1  25738  minveclem3b  25742  ovolficcss  25783  ovolicc2lem4  25834  iundisj2  25863  uniioombllem4  25900  vitalilem5  25926  mbfeqalem1  25955  itg1addlem4  26013  limciun  26207  dvlip2  26308  dv11cn  26314  aalioulem3  26654  pserdvlem2  26748  pserdv  26749  abelthlem2  26752  efif1o  26867  efrlim  27290  lgamgulmlem1  27349  fsumdvdsmul  27515  perfectlem2  27550  noextendseq  28017  nosupno  28053  nosupbnd2lem1  28065  noinfno  28068  noetasuplem4  28086  cuteq1  28196  bdayiun  28294  addbday  28397  oncutlt  28643  oniso  28650  addonbday  28658  bdayn0p1  28748  bdaypw2n0bndlem  28842  setsvtx  29606  uhgredgn0  29699  upgredgss  29703  umgredgss  29704  usgredgss  29733  umgrres1lem  29884  upgrres1  29887  1hegrvtxdg1r  30082  clwlknf1oclwwlknlem3  30667  minvecolem1  31469  sh0le  32035  mdslmd3i  32927  iundisj2f  33177  suppss2f  33225  2ndresdju  33236  fnpreimac  33257  fdifsuppconst  33275  suppss3  33308  iundisj2fi  33382  elrgspnsubrunlem1  33801  erlval  33812  lsmsnorb  33939  extvfvvcl  34160  extvfvcl  34161  esplyind  34200  esplyindfv  34201  esplyfvn  34202  constrextdg2lem  34373  pstmfval  34521  ordtrest2NEW  34548  ldgenpisyslem1  34789  ldgenpisyslem2  34790  omsmeas  34948  sitgclbn  34968  eulerpartlemt  34996  eulerpartlemmf  35000  eulerpartlemgf  35004  bnj849  35548  bnj1136  35620  bnj1311  35647  bnj1413  35658  bnj1452  35675  kardnnfi  35820  rankkardu  35822  vonf1oonfo  35877  blsconn  35988  cvmliftlem2  36030  cvmlift2lem12  36058  mvtss  36297  mthmpps  36326  ellcsrspsn  36385  neibastop2lem  37128  filnetlem3  37148  ttcmin  37264  finxpsuclem  38300  poimirlem3  38521  mblfinlem3  38557  areacirclem2  38607  dfprop2  38626  sdclem1  38657  istotbnd3  38685  sstotbnd  38689  iccbnd  38754  icccmpALT  38755  osumcllem1N  40993  osumcllem2N  40994  osumcllem4N  40996  osumcllem9N  41001  pexmidlem6N  41012  dihglblem3N  42332  dvhdimlem  42481  dochexmidlem6  42502  lcfrlem16  42595  lcfr  42622  aks6d1c6lem3  43202  rhmqusspan  43215  ssabdv  43254  hbtlem6  44115  iocinico  44198  oege2  44293  omabs2  44318  tfsconcatb0  44330  trclubgNEW  44603  cnvrcl0  44610  relexp0a  44701  brtrclfv2  44712  cotrclrcl  44727  frege77d  44731  unhe1  44770  ntrrn  45107  imo72b2lem2  45152  imo72b2  45157  mnuprdlem4  45244  radcnvrat  45283  iunconnlem2  45902  ssinss2d  46046  limccog  46601  limsupresico  46679  liminfresico  46750  icccncfext  46866  stoweidlem14  46993  fourierdlem20  47106  fourierdlem42  47128  fourierdlem46  47131  fourierdlem50  47135  fourierdlem51  47136  fourierdlem54  47139  fourierdlem64  47149  fourierdlem76  47161  fourierdlem102  47187  fourierdlem103  47188  fourierdlem104  47189  fourierdlem114  47199  meadjiunlem  47444  meaiininclem  47465  ovnsupge0  47536  hoidmvlelem2  47575  hoidmvlelem4  47577  vonvolmbllem  47639  vonvolmbl2  47642  vonvol2  47643  vonioolem1  47659  preimageiingt  47699  issmflem  47706  fsupdm  47821  finfdm  47825  fundcmpsurinjimaid  48462  perfectALTVlem2  48789  isubgruhgr  48935  uspgropssxp  49211  rhmsubcALTVlem4  49350  srhmsubcALTV  49391  imasubc  50228  imassc  50230  onsetreclem2  50768