Theorem eqsstrid 3974

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729  df-ss 3920

This theorem is referenced by:  eqsstrrid  3975  3sstr4g  3989  inss  4202  tpssi  4796  opabssxpd  5679  xpsspw  5766  fun  6704  fmpt  7064  fssrescdmd  7081  fliftrel  7264  knatar  7313  fr3nr  7727  ordsuci  7763  fiun  7897  f1iun  7898  1stcof  7973  2ndcof  7974  fsplitfpar  8070  fnwelem  8083  oeeui  8540  cofon1  8610  aceq3lem  10042  cflecard  10175  cfslb2n  10190  itunitc1  10342  axdc2lem  10370  axdc3lem2  10373  fpwwe2lem11  10564  canthwelem  10573  wuncval2  10670  peano5nni  12160  un0addcl  12446  un0mulcl  12447  fsuppmapnn0fiublem  13925  fsuppmapnn0fiub  13926  mertenslem2  15820  4sqlem11  16895  4sqlem19  16903  vdwlem13  16933  imasless  17473  rescfth  17875  oppchofcl  18195  oyoncl  18205  mgmidsssn0  18609  eqg0subg  19137  cycsubm  19143  efgsfo  19680  efgcpbllemb  19696  frgpuplem  19713  gsummpt1n0  19906  dprdfid  19960  dprd2d2  19987  ablfacrp  20009  ablfac1b  20013  ablfac1eu  20016  pgpfac1lem5  20022  ablfaclem3  20030  funcrngcsetc  20585  funcringcsetc  20619  srhmsubc  20625  rhmsubclem3  20632  lsptpcl  20942  lsppratlem3  21116  lsppratlem4  21117  lbsextlem2  21126  f1lindf  21789  topsn  22887  ordtbaslem  23144  ordtuni  23146  ordtbas2  23147  cnpco  23223  cnconst2  23239  tgcmp  23357  iunconn  23384  ptuni2  23532  xkococnlem  23615  tgqtop  23668  fbasrn  23840  uzrest  23853  fmco  23917  alexsubALT  24007  cnextf  24022  snclseqg  24072  ustund  24178  imasdsf1olem  24329  xmetresbl  24393  blsscls2  24460  metustss  24507  tngtopn  24606  reconn  24785  metnrmlem3  24818  cphsubrglem  25145  minveclem1  25392  minveclem3b  25396  ovolficcss  25438  ovolicc2lem4  25489  iundisj2  25518  uniioombllem4  25555  vitalilem5  25581  mbfeqalem1  25610  itg1addlem4  25668  limciun  25863  dvlip2  25968  dv11cn  25974  aalioulem3  26310  pserdvlem2  26406  pserdv  26407  abelthlem2  26410  efif1o  26523  efrlim  26947  efrlimOLD  26948  lgamgulmlem1  27007  fsumdvdsmul  27173  fsumdvdsmulOLD  27175  perfectlem2  27209  noextendseq  27647  nosupno  27683  nosupbnd2lem1  27695  noinfno  27698  noetasuplem4  27716  cuteq1  27825  bdayiun  27923  addbday  28026  oncutlt  28272  oniso  28279  addonbday  28287  bdayn0p1  28377  bdaypw2n0bndlem  28471  setsvtx  29120  uhgredgn0  29213  upgredgss  29217  umgredgss  29218  usgredgss  29244  umgrres1lem  29395  upgrres1  29398  1hegrvtxdg1r  29594  clwlknf1oclwwlknlem3  30170  minvecolem1  30961  sh0le  31527  mdslmd3i  32419  iundisj2f  32676  suppss2f  32727  2ndresdju  32738  fnpreimac  32759  fdifsuppconst  32778  suppss3  32812  iundisj2fi  32887  elrgspnsubrunlem1  33340  erlval  33351  lsmsnorb  33483  extvfvvcl  33711  extvfvcl  33712  esplyind  33751  esplyindfv  33752  esplyfvn  33753  constrextdg2lem  33925  pstmfval  34073  ordtrest2NEW  34100  ldgenpisyslem1  34340  ldgenpisyslem2  34341  omsmeas  34500  sitgclbn  34520  eulerpartlemt  34548  eulerpartlemmf  34552  eulerpartlemgf  34556  bnj849  35100  bnj1136  35172  bnj1311  35199  bnj1413  35210  bnj1452  35227  blsconn  35457  cvmliftlem2  35499  cvmlift2lem12  35527  mvtss  35766  mthmpps  35795  ellcsrspsn  35854  neibastop2lem  36573  filnetlem3  36593  finxpsuclem  37649  poimirlem3  37871  mblfinlem3  37907  areacirclem2  37957  sdclem1  37991  istotbnd3  38019  sstotbnd  38023  iccbnd  38088  icccmpALT  38089  osumcllem1N  40329  osumcllem2N  40330  osumcllem4N  40332  osumcllem9N  40337  pexmidlem6N  40348  dihglblem3N  41668  dvhdimlem  41817  dochexmidlem6  41838  lcfrlem16  41931  lcfr  41958  aks6d1c6lem3  42539  rhmqusspan  42552  ssabdv  42589  hbtlem6  43483  iocinico  43566  oege2  43661  omabs2  43686  tfsconcatb0  43698  trclubgNEW  43971  cnvrcl0  43978  relexp0a  44069  brtrclfv2  44080  cotrclrcl  44095  frege77d  44099  unhe1  44138  ntrrn  44475  imo72b2lem2  44520  imo72b2  44525  mnuprdlem4  44628  radcnvrat  44667  iunconnlem2  45287  ssinss2d  45417  limccog  45977  limsupresico  46055  liminfresico  46126  icccncfext  46242  stoweidlem14  46369  fourierdlem20  46482  fourierdlem42  46504  fourierdlem46  46507  fourierdlem50  46511  fourierdlem51  46512  fourierdlem54  46515  fourierdlem64  46525  fourierdlem76  46537  fourierdlem102  46563  fourierdlem103  46564  fourierdlem104  46565  fourierdlem114  46575  meadjiunlem  46820  meaiininclem  46841  ovnsupge0  46912  hoidmvlelem2  46951  hoidmvlelem4  46953  vonvolmbllem  47015  vonvolmbl2  47018  vonvol2  47019  vonioolem1  47035  preimageiingt  47075  issmflem  47082  fsupdm  47197  finfdm  47201  fundcmpsurinjimaid  47768  perfectALTVlem2  48079  isubgruhgr  48225  uspgropssxp  48501  rhmsubcALTVlem4  48641  srhmsubcALTV  48682  imasubc  49507  imassc  49509  setrec2fun  50048  onsetreclem2  50062