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 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757  df-ss 3923

This theorem is used by:  eqsstrrid  3977  3sstr4g  3991  inss  4201  tpssi  4805  opabssxpd  5710  xpsspw  5798  fun  6744  fmpt  7109  fssrescdmd  7126  fliftrel  7312  knatar  7363  fr3nr  7773  ordsuci  7809  fiun  7942  f1iun  7943  1stcof  8018  2ndcof  8019  fsplitfpar  8115  fnwelem  8129  oeeui  8590  cofon1  8660  aceq3lem  10116  cflecard  10247  cfslb2n  10263  itunitc1  10415  axdc2lem  10443  axdc3lem2  10446  fpwwe2lem11  10637  canthwelem  10646  wuncval2  10743  peano5nni  12247  un0addcl  12548  un0mulcl  12549  fsuppmapnn0fiublem  14039  fsuppmapnn0fiub  14040  mertenslem2  15957  4sqlem11  17032  4sqlem19  17040  vdwlem13  17070  imasless  17611  rescfth  18013  oppchofcl  18333  oyoncl  18343  mgmidsssn0  18748  eqg0subg  19290  cycsubm  19296  efgsfo  19832  efgcpbllemb  19848  frgpuplem  19865  gsummpt1n0  20058  dprdfid  20112  dprd2d2  20139  ablfacrp  20161  ablfac1b  20165  ablfac1eu  20168  pgpfac1lem5  20174  ablfaclem3  20182  funcrngcsetc  20768  funcringcsetc  20802  srhmsubc  20808  rhmsubclem3  20815  lsptpcl  21129  lsppratlem3  21302  lsppratlem4  21303  lbsextlem2  21312  f1lindf  22001  topsn  23117  ordtbaslem  23374  ordtuni  23376  ordtbas2  23377  cnpco  23453  cnconst2  23469  tgcmp  23587  iunconn  23614  ptuni2  23762  xkococnlem  23845  tgqtop  23898  fbasrn  24070  uzrest  24083  fmco  24147  alexsubALT  24237  cnextf  24252  snclseqg  24302  ustund  24408  imasdsf1olem  24559  xmetresbl  24623  blsscls2  24690  metustss  24737  tngtopn  24836  reconn  25015  metnrmlem3  25048  cphsubrglem  25365  minveclem1  25612  minveclem3b  25616  ovolficcss  25657  ovolicc2lem4  25708  iundisj2  25737  uniioombllem4  25774  vitalilem5  25800  mbfeqalem1  25829  itg1addlem4  25887  limciun  26082  dvlip2  26183  dv11cn  26189  aalioulem3  26526  pserdvlem2  26620  pserdv  26621  abelthlem2  26624  efif1o  26740  efrlim  27163  lgamgulmlem1  27222  fsumdvdsmul  27388  perfectlem2  27423  noextendseq  27860  nosupno  27896  nosupbnd2lem1  27908  noinfno  27911  noetasuplem4  27929  cuteq1  28039  bdayiun  28137  addbday  28240  oncutlt  28486  oniso  28493  addonbday  28501  bdayn0p1  28591  bdaypw2n0bndlem  28685  setsvtx  29414  uhgredgn0  29507  upgredgss  29511  umgredgss  29512  usgredgss  29538  umgrres1lem  29689  upgrres1  29692  1hegrvtxdg1r  29887  clwlknf1oclwwlknlem3  30463  minvecolem1  31255  sh0le  31821  mdslmd3i  32713  iundisj2f  32964  suppss2f  33012  2ndresdju  33023  fnpreimac  33044  fdifsuppconst  33063  suppss3  33097  iundisj2fi  33171  elrgspnsubrunlem1  33590  erlval  33601  lsmsnorb  33727  extvfvvcl  33948  extvfvcl  33949  esplyind  33988  esplyindfv  33989  esplyfvn  33990  constrextdg2lem  34161  pstmfval  34309  ordtrest2NEW  34336  ldgenpisyslem1  34577  ldgenpisyslem2  34578  omsmeas  34737  sitgclbn  34757  eulerpartlemt  34785  eulerpartlemmf  34789  eulerpartlemgf  34793  bnj849  35337  bnj1136  35409  bnj1311  35436  bnj1413  35447  bnj1452  35464  kardnnfi  35598  rankkardu  35600  vonf1oonfo  35615  blsconn  35749  cvmliftlem2  35791  cvmlift2lem12  35819  mvtss  36058  mthmpps  36087  ellcsrspsn  36146  neibastop2lem  36904  filnetlem3  36924  ttcmin  37040  finxpsuclem  38076  poimirlem3  38307  mblfinlem3  38343  areacirclem2  38393  sdclem1  38427  istotbnd3  38455  sstotbnd  38459  iccbnd  38524  icccmpALT  38525  osumcllem1N  40763  osumcllem2N  40764  osumcllem4N  40766  osumcllem9N  40771  pexmidlem6N  40782  dihglblem3N  42102  dvhdimlem  42251  dochexmidlem6  42272  lcfrlem16  42365  lcfr  42392  aks6d1c6lem3  42972  rhmqusspan  42985  ssabdv  43024  hbtlem6  43889  iocinico  43972  oege2  44067  omabs2  44092  tfsconcatb0  44104  trclubgNEW  44377  cnvrcl0  44384  relexp0a  44475  brtrclfv2  44486  cotrclrcl  44501  frege77d  44505  unhe1  44544  ntrrn  44881  imo72b2lem2  44926  imo72b2  44931  mnuprdlem4  45018  radcnvrat  45057  iunconnlem2  45676  ssinss2d  45813  limccog  46369  limsupresico  46447  liminfresico  46518  icccncfext  46634  stoweidlem14  46761  fourierdlem20  46874  fourierdlem42  46896  fourierdlem46  46899  fourierdlem50  46903  fourierdlem51  46904  fourierdlem54  46907  fourierdlem64  46917  fourierdlem76  46929  fourierdlem102  46955  fourierdlem103  46956  fourierdlem104  46957  fourierdlem114  46967  meadjiunlem  47212  meaiininclem  47233  ovnsupge0  47304  hoidmvlelem2  47343  hoidmvlelem4  47345  vonvolmbllem  47407  vonvolmbl2  47410  vonvol2  47411  vonioolem1  47427  preimageiingt  47467  issmflem  47474  fsupdm  47589  finfdm  47593  fundcmpsurinjimaid  48193  perfectALTVlem2  48520  isubgruhgr  48666  uspgropssxp  48942  rhmsubcALTVlem4  49082  srhmsubcALTV  49123  imasubc  49962  imassc  49964  setrec2fun  50503  onsetreclem2  50517