Theorem eqsstrid 3997

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

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

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 2707

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

This theorem is referenced by:  eqsstrrid  3998  3sstr4g  4012  inss  4223  tpssi  4814  opabssxpd  5701  xpsspw  5788  fun  6740  fmpt  7100  fssrescdmd  7116  fliftrel  7301  knatar  7350  fr3nr  7766  ordsuci  7802  sucexeloniOLD  7804  suceloniOLD  7806  fiun  7941  f1iun  7942  1stcof  8018  2ndcof  8019  fsplitfpar  8117  fnwelem  8130  oeeui  8614  cofon1  8684  aceq3lem  10134  cflecard  10267  cfslb2n  10282  itunitc1  10434  axdc3lem2  10465  fpwwe2lem11  10655  canthwelem  10664  wuncval2  10761  peano5nni  12243  un0addcl  12534  un0mulcl  12535  fsuppmapnn0fiublem  14008  fsuppmapnn0fiub  14009  mertenslem2  15901  4sqlem11  16975  4sqlem19  16983  vdwlem13  17013  imasless  17554  rescfth  17952  oppchofcl  18272  oyoncl  18282  mgmidsssn0  18650  eqg0subg  19179  cycsubm  19185  efgsfo  19720  efgcpbllemb  19736  frgpuplem  19753  gsummpt1n0  19946  dprdfid  20000  dprd2d2  20027  ablfacrp  20049  ablfac1b  20053  ablfac1eu  20056  pgpfac1lem5  20062  ablfaclem3  20070  funcrngcsetc  20600  funcringcsetc  20634  srhmsubc  20640  rhmsubclem3  20647  lsptpcl  20936  lsppratlem3  21110  lsppratlem4  21111  lbsextlem2  21120  f1lindf  21782  topsn  22869  ordtbaslem  23126  ordtuni  23128  ordtbas2  23129  cnpco  23205  cnconst2  23221  tgcmp  23339  iunconn  23366  ptuni2  23514  xkococnlem  23597  tgqtop  23650  fbasrn  23822  uzrest  23835  fmco  23899  alexsubALT  23989  cnextf  24004  snclseqg  24054  ustund  24160  imasdsf1olem  24312  xmetresbl  24376  blsscls2  24443  metustss  24490  tngtopn  24589  reconn  24768  metnrmlem3  24801  cphsubrglem  25129  minveclem1  25376  minveclem3b  25380  ovolficcss  25422  ovolicc2lem4  25473  iundisj2  25502  uniioombllem4  25539  vitalilem5  25565  mbfeqalem1  25594  itg1addlem4  25652  limciun  25847  dvlip2  25952  dv11cn  25958  aalioulem3  26294  pserdvlem2  26390  pserdv  26391  abelthlem2  26394  efif1o  26507  efrlim  26931  efrlimOLD  26932  lgamgulmlem1  26991  fsumdvdsmul  27157  fsumdvdsmulOLD  27159  perfectlem2  27193  noextendseq  27631  nosupno  27667  nosupbnd2lem1  27679  noinfno  27682  noetasuplem4  27700  cuteq1  27798  addsbday  27976  onscutlt  28217  onsiso  28221  bdayn0p1  28310  setsvtx  29014  uhgredgn0  29107  upgredgss  29111  umgredgss  29112  usgredgss  29138  umgrres1lem  29289  upgrres1  29292  1hegrvtxdg1r  29488  clwlknf1oclwwlknlem3  30064  minvecolem1  30855  sh0le  31421  mdslmd3i  32313  iundisj2f  32571  suppss2f  32616  2ndresdju  32627  fnpreimac  32649  fdifsuppconst  32666  suppss3  32701  iundisj2fi  32774  elrgspnsubrunlem1  33242  erlval  33253  lsmsnorb  33406  constrextdg2lem  33782  pstmfval  33927  ordtrest2NEW  33954  ldgenpisyslem1  34194  ldgenpisyslem2  34195  omsmeas  34355  sitgclbn  34375  eulerpartlemt  34403  eulerpartlemmf  34407  eulerpartlemgf  34411  bnj849  34956  bnj1136  35028  bnj1311  35055  bnj1413  35066  bnj1452  35083  blsconn  35266  cvmliftlem2  35308  cvmlift2lem12  35336  mvtss  35575  mthmpps  35604  ellcsrspsn  35663  neibastop2lem  36378  filnetlem3  36398  finxpsuclem  37415  poimirlem3  37647  mblfinlem3  37683  areacirclem2  37733  sdclem1  37767  istotbnd3  37795  sstotbnd  37799  iccbnd  37864  icccmpALT  37865  osumcllem1N  39975  osumcllem2N  39976  osumcllem4N  39978  osumcllem9N  39983  pexmidlem6N  39994  dihglblem3N  41314  dvhdimlem  41463  dochexmidlem6  41484  lcfrlem16  41577  lcfr  41604  aks6d1c6lem3  42185  rhmqusspan  42198  ssabdv  42271  hbtlem6  43153  iocinico  43236  oege2  43331  omabs2  43356  tfsconcatb0  43368  trclubgNEW  43642  cnvrcl0  43649  relexp0a  43740  brtrclfv2  43751  cotrclrcl  43766  frege77d  43770  unhe1  43809  ntrrn  44146  imo72b2lem2  44191  imo72b2  44196  mnuprdlem4  44299  radcnvrat  44338  iunconnlem2  44959  ssinss2d  45084  limccog  45649  limsupresico  45729  liminfresico  45800  icccncfext  45916  stoweidlem14  46043  fourierdlem20  46156  fourierdlem42  46178  fourierdlem46  46181  fourierdlem50  46185  fourierdlem51  46186  fourierdlem54  46189  fourierdlem64  46199  fourierdlem76  46211  fourierdlem102  46237  fourierdlem103  46238  fourierdlem104  46239  fourierdlem114  46249  meadjiunlem  46494  meaiininclem  46515  ovnsupge0  46586  hoidmvlelem2  46625  hoidmvlelem4  46627  vonvolmbllem  46689  vonvolmbl2  46692  vonvol2  46693  vonioolem1  46709  issmflem  46756  fsupdm  46871  finfdm  46875  fundcmpsurinjimaid  47425  perfectALTVlem2  47736  isubgruhgr  47881  uspgropssxp  48119  rhmsubcALTVlem4  48259  srhmsubcALTV  48300  imasubc  49091  imassc  49093  setrec2fun  49556  onsetreclem2  49570