Theorem eqsstrid 3976

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

Syntax hints:   → wi 4   = wceq 1570   ⊆ wss 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-ex 1810  df-cleq 2755  df-ss 3923

This theorem is referenced by:  eqsstrrid  3977  3sstr4g  3991  inss  4202  tpssi  4804  opabssxpd  5710  xpsspw  5798  fun  6742  fmpt  7107  fssrescdmd  7124  fliftrel  7308  knatar  7357  fr3nr  7772  ordsuci  7808  fiun  7941  f1iun  7942  1stcof  8017  2ndcof  8018  fsplitfpar  8114  fnwelem  8128  oeeui  8589  cofon1  8659  aceq3lem  10105  cflecard  10237  cfslb2n  10253  itunitc1  10405  axdc2lem  10433  axdc3lem2  10436  fpwwe2lem11  10627  canthwelem  10636  wuncval2  10733  peano5nni  12237  un0addcl  12538  un0mulcl  12539  fsuppmapnn0fiublem  14028  fsuppmapnn0fiub  14029  mertenslem2  15941  4sqlem11  17016  4sqlem19  17024  vdwlem13  17054  imasless  17595  rescfth  17997  oppchofcl  18317  oyoncl  18327  mgmidsssn0  18731  eqg0subg  19268  cycsubm  19274  efgsfo  19810  efgcpbllemb  19826  frgpuplem  19843  gsummpt1n0  20036  dprdfid  20090  dprd2d2  20117  ablfacrp  20139  ablfac1b  20143  ablfac1eu  20146  pgpfac1lem5  20152  ablfaclem3  20160  funcrngcsetc  20726  funcringcsetc  20760  srhmsubc  20766  rhmsubclem3  20773  lsptpcl  21081  lsppratlem3  21254  lsppratlem4  21255  lbsextlem2  21264  f1lindf  21953  topsn  23069  ordtbaslem  23326  ordtuni  23328  ordtbas2  23329  cnpco  23405  cnconst2  23421  tgcmp  23539  iunconn  23566  ptuni2  23714  xkococnlem  23797  tgqtop  23850  fbasrn  24022  uzrest  24035  fmco  24099  alexsubALT  24189  cnextf  24204  snclseqg  24254  ustund  24360  imasdsf1olem  24511  xmetresbl  24575  blsscls2  24642  metustss  24689  tngtopn  24788  reconn  24967  metnrmlem3  25000  cphsubrglem  25317  minveclem1  25564  minveclem3b  25568  ovolficcss  25609  ovolicc2lem4  25660  iundisj2  25689  uniioombllem4  25726  vitalilem5  25752  mbfeqalem1  25781  itg1addlem4  25839  limciun  26034  dvlip2  26135  dv11cn  26141  aalioulem3  26478  pserdvlem2  26572  pserdv  26573  abelthlem2  26576  efif1o  26692  efrlim  27115  lgamgulmlem1  27174  fsumdvdsmul  27340  perfectlem2  27375  noextendseq  27812  nosupno  27848  nosupbnd2lem1  27860  noinfno  27863  noetasuplem4  27881  cuteq1  27991  bdayiun  28089  addbday  28192  oncutlt  28438  oniso  28445  addonbday  28453  bdayn0p1  28543  bdaypw2n0bndlem  28637  setsvtx  29366  uhgredgn0  29459  upgredgss  29463  umgredgss  29464  usgredgss  29490  umgrres1lem  29641  upgrres1  29644  1hegrvtxdg1r  29839  clwlknf1oclwwlknlem3  30415  minvecolem1  31207  sh0le  31773  mdslmd3i  32665  iundisj2f  32916  suppss2f  32964  2ndresdju  32975  fnpreimac  32996  fdifsuppconst  33015  suppss3  33049  iundisj2fi  33123  elrgspnsubrunlem1  33548  erlval  33559  lsmsnorb  33685  extvfvvcl  33906  extvfvcl  33907  esplyind  33946  esplyindfv  33947  esplyfvn  33948  constrextdg2lem  34119  pstmfval  34267  ordtrest2NEW  34294  ldgenpisyslem1  34534  ldgenpisyslem2  34535  omsmeas  34694  sitgclbn  34714  eulerpartlemt  34742  eulerpartlemmf  34746  eulerpartlemgf  34750  bnj849  35294  bnj1136  35366  bnj1311  35393  bnj1413  35404  bnj1452  35421  kardnnfi  35563  rankkardu  35565  vonf1oonfo  35580  blsconn  35717  cvmliftlem2  35759  cvmlift2lem12  35787  mvtss  36026  mthmpps  36055  ellcsrspsn  36114  neibastop2lem  36852  filnetlem3  36872  ttcmin  36988  finxpsuclem  38024  poimirlem3  38255  mblfinlem3  38291  areacirclem2  38341  sdclem1  38375  istotbnd3  38403  sstotbnd  38407  iccbnd  38472  icccmpALT  38473  osumcllem1N  40711  osumcllem2N  40712  osumcllem4N  40714  osumcllem9N  40719  pexmidlem6N  40730  dihglblem3N  42050  dvhdimlem  42199  dochexmidlem6  42220  lcfrlem16  42313  lcfr  42340  aks6d1c6lem3  42920  rhmqusspan  42933  ssabdv  42972  hbtlem6  43839  iocinico  43922  oege2  44017  omabs2  44042  tfsconcatb0  44054  trclubgNEW  44327  cnvrcl0  44334  relexp0a  44425  brtrclfv2  44436  cotrclrcl  44451  frege77d  44455  unhe1  44494  ntrrn  44831  imo72b2lem2  44876  imo72b2  44881  mnuprdlem4  44968  radcnvrat  45007  iunconnlem2  45626  ssinss2d  45763  limccog  46319  limsupresico  46397  liminfresico  46468  icccncfext  46584  stoweidlem14  46711  fourierdlem20  46824  fourierdlem42  46846  fourierdlem46  46849  fourierdlem50  46853  fourierdlem51  46854  fourierdlem54  46857  fourierdlem64  46867  fourierdlem76  46879  fourierdlem102  46905  fourierdlem103  46906  fourierdlem104  46907  fourierdlem114  46917  meadjiunlem  47162  meaiininclem  47183  ovnsupge0  47254  hoidmvlelem2  47293  hoidmvlelem4  47295  vonvolmbllem  47357  vonvolmbl2  47360  vonvol2  47361  vonioolem1  47377  preimageiingt  47417  issmflem  47424  fsupdm  47539  finfdm  47543  fundcmpsurinjimaid  48143  perfectALTVlem2  48470  isubgruhgr  48616  uspgropssxp  48892  rhmsubcALTVlem4  49032  srhmsubcALTV  49073  imasubc  49912  imassc  49914  setrec2fun  50453  onsetreclem2  50467