Theorem eqsstrid 3985

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

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

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 3931

This theorem is referenced by:  eqsstrrid  3986  3sstr4g  4000  inss  4211  tpssi  4802  opabssxpd  5685  xpsspw  5772  fun  6722  fmpt  7082  fssrescdmd  7098  fliftrel  7283  knatar  7332  fr3nr  7748  ordsuci  7784  sucexeloniOLD  7786  fiun  7921  f1iun  7922  1stcof  7998  2ndcof  7999  fsplitfpar  8097  fnwelem  8110  oeeui  8566  cofon1  8636  aceq3lem  10073  cflecard  10206  cfslb2n  10221  itunitc1  10373  axdc3lem2  10404  fpwwe2lem11  10594  canthwelem  10603  wuncval2  10700  peano5nni  12189  un0addcl  12475  un0mulcl  12476  fsuppmapnn0fiublem  13955  fsuppmapnn0fiub  13956  mertenslem2  15851  4sqlem11  16926  4sqlem19  16934  vdwlem13  16964  imasless  17503  rescfth  17901  oppchofcl  18221  oyoncl  18231  mgmidsssn0  18599  eqg0subg  19128  cycsubm  19134  efgsfo  19669  efgcpbllemb  19685  frgpuplem  19702  gsummpt1n0  19895  dprdfid  19949  dprd2d2  19976  ablfacrp  19998  ablfac1b  20002  ablfac1eu  20005  pgpfac1lem5  20011  ablfaclem3  20019  funcrngcsetc  20549  funcringcsetc  20583  srhmsubc  20589  rhmsubclem3  20596  lsptpcl  20885  lsppratlem3  21059  lsppratlem4  21060  lbsextlem2  21069  f1lindf  21731  topsn  22818  ordtbaslem  23075  ordtuni  23077  ordtbas2  23078  cnpco  23154  cnconst2  23170  tgcmp  23288  iunconn  23315  ptuni2  23463  xkococnlem  23546  tgqtop  23599  fbasrn  23771  uzrest  23784  fmco  23848  alexsubALT  23938  cnextf  23953  snclseqg  24003  ustund  24109  imasdsf1olem  24261  xmetresbl  24325  blsscls2  24392  metustss  24439  tngtopn  24538  reconn  24717  metnrmlem3  24750  cphsubrglem  25077  minveclem1  25324  minveclem3b  25328  ovolficcss  25370  ovolicc2lem4  25421  iundisj2  25450  uniioombllem4  25487  vitalilem5  25513  mbfeqalem1  25542  itg1addlem4  25600  limciun  25795  dvlip2  25900  dv11cn  25906  aalioulem3  26242  pserdvlem2  26338  pserdv  26339  abelthlem2  26342  efif1o  26455  efrlim  26879  efrlimOLD  26880  lgamgulmlem1  26939  fsumdvdsmul  27105  fsumdvdsmulOLD  27107  perfectlem2  27141  noextendseq  27579  nosupno  27615  nosupbnd2lem1  27627  noinfno  27630  noetasuplem4  27648  cuteq1  27746  addsbday  27924  onscutlt  28165  onsiso  28169  bdayn0p1  28258  setsvtx  28962  uhgredgn0  29055  upgredgss  29059  umgredgss  29060  usgredgss  29086  umgrres1lem  29237  upgrres1  29240  1hegrvtxdg1r  29436  clwlknf1oclwwlknlem3  30012  minvecolem1  30803  sh0le  31369  mdslmd3i  32261  iundisj2f  32519  suppss2f  32562  2ndresdju  32573  fnpreimac  32595  fdifsuppconst  32612  suppss3  32647  iundisj2fi  32720  elrgspnsubrunlem1  33198  erlval  33209  lsmsnorb  33362  constrextdg2lem  33738  pstmfval  33886  ordtrest2NEW  33913  ldgenpisyslem1  34153  ldgenpisyslem2  34154  omsmeas  34314  sitgclbn  34334  eulerpartlemt  34362  eulerpartlemmf  34366  eulerpartlemgf  34370  bnj849  34915  bnj1136  34987  bnj1311  35014  bnj1413  35025  bnj1452  35042  blsconn  35231  cvmliftlem2  35273  cvmlift2lem12  35301  mvtss  35540  mthmpps  35569  ellcsrspsn  35628  neibastop2lem  36348  filnetlem3  36368  finxpsuclem  37385  poimirlem3  37617  mblfinlem3  37653  areacirclem2  37703  sdclem1  37737  istotbnd3  37765  sstotbnd  37769  iccbnd  37834  icccmpALT  37835  osumcllem1N  39950  osumcllem2N  39951  osumcllem4N  39953  osumcllem9N  39958  pexmidlem6N  39969  dihglblem3N  41289  dvhdimlem  41438  dochexmidlem6  41459  lcfrlem16  41552  lcfr  41579  aks6d1c6lem3  42160  rhmqusspan  42173  ssabdv  42208  hbtlem6  43118  iocinico  43201  oege2  43296  omabs2  43321  tfsconcatb0  43333  trclubgNEW  43607  cnvrcl0  43614  relexp0a  43705  brtrclfv2  43716  cotrclrcl  43731  frege77d  43735  unhe1  43774  ntrrn  44111  imo72b2lem2  44156  imo72b2  44161  mnuprdlem4  44264  radcnvrat  44303  iunconnlem2  44924  ssinss2d  45054  limccog  45618  limsupresico  45698  liminfresico  45769  icccncfext  45885  stoweidlem14  46012  fourierdlem20  46125  fourierdlem42  46147  fourierdlem46  46150  fourierdlem50  46154  fourierdlem51  46155  fourierdlem54  46158  fourierdlem64  46168  fourierdlem76  46180  fourierdlem102  46206  fourierdlem103  46207  fourierdlem104  46208  fourierdlem114  46218  meadjiunlem  46463  meaiininclem  46484  ovnsupge0  46555  hoidmvlelem2  46594  hoidmvlelem4  46596  vonvolmbllem  46658  vonvolmbl2  46661  vonvol2  46662  vonioolem1  46678  issmflem  46725  fsupdm  46840  finfdm  46844  fundcmpsurinjimaid  47412  perfectALTVlem2  47723  isubgruhgr  47868  uspgropssxp  48132  rhmsubcALTVlem4  48272  srhmsubcALTV  48313  imasubc  49140  imassc  49142  setrec2fun  49681  onsetreclem2  49695