Theorem eqsstrid 4022

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

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

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 2007  ax-9 2118  ax-ext 2708

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

This theorem is referenced by:  eqsstrrid  4023  3sstr4g  4037  inss  4248  tpssi  4838  opabssxpd  5732  xpsspw  5819  fun  6770  fmpt  7130  fssrescdmd  7146  fliftrel  7328  knatar  7377  fr3nr  7792  ordsuci  7828  sucexeloniOLD  7830  suceloniOLD  7832  fiun  7967  f1iun  7968  1stcof  8044  2ndcof  8045  fsplitfpar  8143  fnwelem  8156  oeeui  8640  cofon1  8710  aceq3lem  10160  cflecard  10293  cfslb2n  10308  itunitc1  10460  axdc3lem2  10491  fpwwe2lem11  10681  canthwelem  10690  wuncval2  10787  peano5nni  12269  un0addcl  12559  un0mulcl  12560  fsuppmapnn0fiublem  14031  fsuppmapnn0fiub  14032  mertenslem2  15921  4sqlem11  16993  4sqlem19  17001  vdwlem13  17031  imasless  17585  rescfth  17984  oppchofcl  18305  oyoncl  18315  mgmidsssn0  18685  eqg0subg  19214  cycsubm  19220  efgsfo  19757  efgcpbllemb  19773  frgpuplem  19790  gsummpt1n0  19983  dprdfid  20037  dprd2d2  20064  ablfacrp  20086  ablfac1b  20090  ablfac1eu  20093  pgpfac1lem5  20099  ablfaclem3  20107  funcrngcsetc  20640  funcringcsetc  20674  srhmsubc  20680  rhmsubclem3  20687  lsptpcl  20977  lsppratlem3  21151  lsppratlem4  21152  lbsextlem2  21161  f1lindf  21842  topsn  22937  ordtbaslem  23196  ordtuni  23198  ordtbas2  23199  cnpco  23275  cnconst2  23291  tgcmp  23409  iunconn  23436  ptuni2  23584  xkococnlem  23667  tgqtop  23720  fbasrn  23892  uzrest  23905  fmco  23969  alexsubALT  24059  cnextf  24074  snclseqg  24124  ustund  24230  imasdsf1olem  24383  xmetresbl  24447  blsscls2  24517  metustss  24564  tngtopn  24671  reconn  24850  metnrmlem3  24883  cphsubrglem  25211  minveclem1  25458  minveclem3b  25462  ovolficcss  25504  ovolicc2lem4  25555  iundisj2  25584  uniioombllem4  25621  vitalilem5  25647  mbfeqalem1  25676  itg1addlem4  25734  limciun  25929  dvlip2  26034  dv11cn  26040  aalioulem3  26376  pserdvlem2  26472  pserdv  26473  abelthlem2  26476  efif1o  26588  efrlim  27012  efrlimOLD  27013  lgamgulmlem1  27072  fsumdvdsmul  27238  fsumdvdsmulOLD  27240  perfectlem2  27274  noextendseq  27712  nosupno  27748  nosupbnd2lem1  27760  noinfno  27763  noetasuplem4  27781  cuteq1  27878  addsbday  28050  setsvtx  29052  uhgredgn0  29145  upgredgss  29149  umgredgss  29150  usgredgss  29176  umgrres1lem  29327  upgrres1  29330  1hegrvtxdg1r  29526  clwlknf1oclwwlknlem3  30102  minvecolem1  30893  sh0le  31459  mdslmd3i  32351  iundisj2f  32603  suppss2f  32648  2ndresdju  32659  fnpreimac  32681  fdifsuppconst  32698  suppss3  32735  iundisj2fi  32799  elrgspnsubrunlem1  33251  erlval  33262  lsmsnorb  33419  constrextdg2lem  33789  pstmfval  33895  ordtrest2NEW  33922  ldgenpisyslem1  34164  ldgenpisyslem2  34165  omsmeas  34325  sitgclbn  34345  eulerpartlemt  34373  eulerpartlemmf  34377  eulerpartlemgf  34381  bnj849  34939  bnj1136  35011  bnj1311  35038  bnj1413  35049  bnj1452  35066  blsconn  35249  cvmliftlem2  35291  cvmlift2lem12  35319  mvtss  35558  mthmpps  35587  ellcsrspsn  35646  neibastop2lem  36361  filnetlem3  36381  finxpsuclem  37398  poimirlem3  37630  mblfinlem3  37666  areacirclem2  37716  sdclem1  37750  istotbnd3  37778  sstotbnd  37782  iccbnd  37847  icccmpALT  37848  osumcllem1N  39958  osumcllem2N  39959  osumcllem4N  39961  osumcllem9N  39966  pexmidlem6N  39977  dihglblem3N  41297  dvhdimlem  41446  dochexmidlem6  41467  lcfrlem16  41560  lcfr  41587  aks6d1c6lem3  42173  rhmqusspan  42186  ssabdv  42259  hbtlem6  43141  iocinico  43224  oege2  43320  omabs2  43345  tfsconcatb0  43357  trclubgNEW  43631  cnvrcl0  43638  relexp0a  43729  brtrclfv2  43740  cotrclrcl  43755  frege77d  43759  unhe1  43798  ntrrn  44135  imo72b2lem2  44180  imo72b2  44185  mnuprdlem4  44294  radcnvrat  44333  iunconnlem2  44955  ssinss2d  45065  limccog  45635  limsupresico  45715  liminfresico  45786  icccncfext  45902  stoweidlem14  46029  fourierdlem20  46142  fourierdlem42  46164  fourierdlem46  46167  fourierdlem50  46171  fourierdlem51  46172  fourierdlem54  46175  fourierdlem64  46185  fourierdlem76  46197  fourierdlem102  46223  fourierdlem103  46224  fourierdlem104  46225  fourierdlem114  46235  meadjiunlem  46480  meaiininclem  46501  ovnsupge0  46572  hoidmvlelem2  46611  hoidmvlelem4  46613  vonvolmbllem  46675  vonvolmbl2  46678  vonvol2  46679  vonioolem1  46695  issmflem  46742  fsupdm  46857  finfdm  46861  fundcmpsurinjimaid  47398  perfectALTVlem2  47709  isubgruhgr  47854  uspgropssxp  48060  rhmsubcALTVlem4  48200  srhmsubcALTV  48241  setrec2fun  49211  onsetreclem2  49225