Theorem eqsstrid 3982

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721  df-ss 3928

This theorem is referenced by:  eqsstrrid  3983  3sstr4g  3997  inss  4207  tpssi  4798  opabssxpd  5678  xpsspw  5763  fun  6704  fmpt  7064  fssrescdmd  7080  fliftrel  7265  knatar  7314  fr3nr  7728  ordsuci  7764  sucexeloniOLD  7766  fiun  7901  f1iun  7902  1stcof  7977  2ndcof  7978  fsplitfpar  8074  fnwelem  8087  oeeui  8543  cofon1  8613  aceq3lem  10049  cflecard  10182  cfslb2n  10197  itunitc1  10349  axdc3lem2  10380  fpwwe2lem11  10570  canthwelem  10579  wuncval2  10676  peano5nni  12165  un0addcl  12451  un0mulcl  12452  fsuppmapnn0fiublem  13931  fsuppmapnn0fiub  13932  mertenslem2  15827  4sqlem11  16902  4sqlem19  16910  vdwlem13  16940  imasless  17479  rescfth  17877  oppchofcl  18197  oyoncl  18207  mgmidsssn0  18575  eqg0subg  19104  cycsubm  19110  efgsfo  19645  efgcpbllemb  19661  frgpuplem  19678  gsummpt1n0  19871  dprdfid  19925  dprd2d2  19952  ablfacrp  19974  ablfac1b  19978  ablfac1eu  19981  pgpfac1lem5  19987  ablfaclem3  19995  funcrngcsetc  20525  funcringcsetc  20559  srhmsubc  20565  rhmsubclem3  20572  lsptpcl  20861  lsppratlem3  21035  lsppratlem4  21036  lbsextlem2  21045  f1lindf  21707  topsn  22794  ordtbaslem  23051  ordtuni  23053  ordtbas2  23054  cnpco  23130  cnconst2  23146  tgcmp  23264  iunconn  23291  ptuni2  23439  xkococnlem  23522  tgqtop  23575  fbasrn  23747  uzrest  23760  fmco  23824  alexsubALT  23914  cnextf  23929  snclseqg  23979  ustund  24085  imasdsf1olem  24237  xmetresbl  24301  blsscls2  24368  metustss  24415  tngtopn  24514  reconn  24693  metnrmlem3  24726  cphsubrglem  25053  minveclem1  25300  minveclem3b  25304  ovolficcss  25346  ovolicc2lem4  25397  iundisj2  25426  uniioombllem4  25463  vitalilem5  25489  mbfeqalem1  25518  itg1addlem4  25576  limciun  25771  dvlip2  25876  dv11cn  25882  aalioulem3  26218  pserdvlem2  26314  pserdv  26315  abelthlem2  26318  efif1o  26431  efrlim  26855  efrlimOLD  26856  lgamgulmlem1  26915  fsumdvdsmul  27081  fsumdvdsmulOLD  27083  perfectlem2  27117  noextendseq  27555  nosupno  27591  nosupbnd2lem1  27603  noinfno  27606  noetasuplem4  27624  cuteq1  27722  addsbday  27900  onscutlt  28141  onsiso  28145  bdayn0p1  28234  setsvtx  28938  uhgredgn0  29031  upgredgss  29035  umgredgss  29036  usgredgss  29062  umgrres1lem  29213  upgrres1  29216  1hegrvtxdg1r  29412  clwlknf1oclwwlknlem3  29985  minvecolem1  30776  sh0le  31342  mdslmd3i  32234  iundisj2f  32492  suppss2f  32535  2ndresdju  32546  fnpreimac  32568  fdifsuppconst  32585  suppss3  32620  iundisj2fi  32693  elrgspnsubrunlem1  33171  erlval  33182  lsmsnorb  33335  constrextdg2lem  33711  pstmfval  33859  ordtrest2NEW  33886  ldgenpisyslem1  34126  ldgenpisyslem2  34127  omsmeas  34287  sitgclbn  34307  eulerpartlemt  34335  eulerpartlemmf  34339  eulerpartlemgf  34343  bnj849  34888  bnj1136  34960  bnj1311  34987  bnj1413  34998  bnj1452  35015  blsconn  35204  cvmliftlem2  35246  cvmlift2lem12  35274  mvtss  35513  mthmpps  35542  ellcsrspsn  35601  neibastop2lem  36321  filnetlem3  36341  finxpsuclem  37358  poimirlem3  37590  mblfinlem3  37626  areacirclem2  37676  sdclem1  37710  istotbnd3  37738  sstotbnd  37742  iccbnd  37807  icccmpALT  37808  osumcllem1N  39923  osumcllem2N  39924  osumcllem4N  39926  osumcllem9N  39931  pexmidlem6N  39942  dihglblem3N  41262  dvhdimlem  41411  dochexmidlem6  41432  lcfrlem16  41525  lcfr  41552  aks6d1c6lem3  42133  rhmqusspan  42146  ssabdv  42181  hbtlem6  43091  iocinico  43174  oege2  43269  omabs2  43294  tfsconcatb0  43306  trclubgNEW  43580  cnvrcl0  43587  relexp0a  43678  brtrclfv2  43689  cotrclrcl  43704  frege77d  43708  unhe1  43747  ntrrn  44084  imo72b2lem2  44129  imo72b2  44134  mnuprdlem4  44237  radcnvrat  44276  iunconnlem2  44897  ssinss2d  45027  limccog  45591  limsupresico  45671  liminfresico  45742  icccncfext  45858  stoweidlem14  45985  fourierdlem20  46098  fourierdlem42  46120  fourierdlem46  46123  fourierdlem50  46127  fourierdlem51  46128  fourierdlem54  46131  fourierdlem64  46141  fourierdlem76  46153  fourierdlem102  46179  fourierdlem103  46180  fourierdlem104  46181  fourierdlem114  46191  meadjiunlem  46436  meaiininclem  46457  ovnsupge0  46528  hoidmvlelem2  46567  hoidmvlelem4  46569  vonvolmbllem  46631  vonvolmbl2  46634  vonvol2  46635  vonioolem1  46651  issmflem  46698  fsupdm  46813  finfdm  46817  fundcmpsurinjimaid  47385  perfectALTVlem2  47696  isubgruhgr  47841  uspgropssxp  48105  rhmsubcALTVlem4  48245  srhmsubcALTV  48286  imasubc  49113  imassc  49115  setrec2fun  49654  onsetreclem2  49668