Theorem eqsstrid 3961

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

Syntax hints:   → wi 4   = wceq 1542   ⊆ wss 3890

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

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

This theorem is referenced by:  eqsstrrid  3962  3sstr4g  3976  inss  4189  tpssi  4782  opabssxpd  5671  xpsspw  5758  fun  6696  fmpt  7056  fssrescdmd  7073  fliftrel  7256  knatar  7305  fr3nr  7719  ordsuci  7755  fiun  7889  f1iun  7890  1stcof  7965  2ndcof  7966  fsplitfpar  8061  fnwelem  8074  oeeui  8531  cofon1  8601  aceq3lem  10033  cflecard  10166  cfslb2n  10181  itunitc1  10333  axdc2lem  10361  axdc3lem2  10364  fpwwe2lem11  10555  canthwelem  10564  wuncval2  10661  peano5nni  12168  un0addcl  12461  un0mulcl  12462  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  mertenslem2  15841  4sqlem11  16917  4sqlem19  16925  vdwlem13  16955  imasless  17495  rescfth  17897  oppchofcl  18217  oyoncl  18227  mgmidsssn0  18631  eqg0subg  19162  cycsubm  19168  efgsfo  19705  efgcpbllemb  19721  frgpuplem  19738  gsummpt1n0  19931  dprdfid  19985  dprd2d2  20012  ablfacrp  20034  ablfac1b  20038  ablfac1eu  20041  pgpfac1lem5  20047  ablfaclem3  20055  funcrngcsetc  20608  funcringcsetc  20642  srhmsubc  20648  rhmsubclem3  20655  lsptpcl  20965  lsppratlem3  21139  lsppratlem4  21140  lbsextlem2  21149  f1lindf  21812  topsn  22906  ordtbaslem  23163  ordtuni  23165  ordtbas2  23166  cnpco  23242  cnconst2  23258  tgcmp  23376  iunconn  23403  ptuni2  23551  xkococnlem  23634  tgqtop  23687  fbasrn  23859  uzrest  23872  fmco  23936  alexsubALT  24026  cnextf  24041  snclseqg  24091  ustund  24197  imasdsf1olem  24348  xmetresbl  24412  blsscls2  24479  metustss  24526  tngtopn  24625  reconn  24804  metnrmlem3  24837  cphsubrglem  25154  minveclem1  25401  minveclem3b  25405  ovolficcss  25446  ovolicc2lem4  25497  iundisj2  25526  uniioombllem4  25563  vitalilem5  25589  mbfeqalem1  25618  itg1addlem4  25676  limciun  25871  dvlip2  25972  dv11cn  25978  aalioulem3  26311  pserdvlem2  26406  pserdv  26407  abelthlem2  26410  efif1o  26523  efrlim  26946  efrlimOLD  26947  lgamgulmlem1  27006  fsumdvdsmul  27172  perfectlem2  27207  noextendseq  27645  nosupno  27681  nosupbnd2lem1  27693  noinfno  27696  noetasuplem4  27714  cuteq1  27823  bdayiun  27921  addbday  28024  oncutlt  28270  oniso  28277  addonbday  28285  bdayn0p1  28375  bdaypw2n0bndlem  28469  setsvtx  29118  uhgredgn0  29211  upgredgss  29215  umgredgss  29216  usgredgss  29242  umgrres1lem  29393  upgrres1  29396  1hegrvtxdg1r  29592  clwlknf1oclwwlknlem3  30168  minvecolem1  30960  sh0le  31526  mdslmd3i  32418  iundisj2f  32675  suppss2f  32726  2ndresdju  32737  fnpreimac  32758  fdifsuppconst  32777  suppss3  32811  iundisj2fi  32885  elrgspnsubrunlem1  33323  erlval  33334  lsmsnorb  33466  extvfvvcl  33694  extvfvcl  33695  esplyind  33734  esplyindfv  33735  esplyfvn  33736  constrextdg2lem  33908  pstmfval  34056  ordtrest2NEW  34083  ldgenpisyslem1  34323  ldgenpisyslem2  34324  omsmeas  34483  sitgclbn  34503  eulerpartlemt  34531  eulerpartlemmf  34535  eulerpartlemgf  34539  bnj849  35083  bnj1136  35155  bnj1311  35182  bnj1413  35193  bnj1452  35210  blsconn  35442  cvmliftlem2  35484  cvmlift2lem12  35512  mvtss  35751  mthmpps  35780  ellcsrspsn  35839  neibastop2lem  36558  filnetlem3  36578  ttcmin  36694  finxpsuclem  37727  poimirlem3  37958  mblfinlem3  37994  areacirclem2  38044  sdclem1  38078  istotbnd3  38106  sstotbnd  38110  iccbnd  38175  icccmpALT  38176  osumcllem1N  40416  osumcllem2N  40417  osumcllem4N  40419  osumcllem9N  40424  pexmidlem6N  40435  dihglblem3N  41755  dvhdimlem  41904  dochexmidlem6  41925  lcfrlem16  42018  lcfr  42045  aks6d1c6lem3  42625  rhmqusspan  42638  ssabdv  42675  hbtlem6  43575  iocinico  43658  oege2  43753  omabs2  43778  tfsconcatb0  43790  trclubgNEW  44063  cnvrcl0  44070  relexp0a  44161  brtrclfv2  44172  cotrclrcl  44187  frege77d  44191  unhe1  44230  ntrrn  44567  imo72b2lem2  44612  imo72b2  44617  mnuprdlem4  44720  radcnvrat  44759  iunconnlem2  45379  ssinss2d  45509  limccog  46068  limsupresico  46146  liminfresico  46217  icccncfext  46333  stoweidlem14  46460  fourierdlem20  46573  fourierdlem42  46595  fourierdlem46  46598  fourierdlem50  46602  fourierdlem51  46603  fourierdlem54  46606  fourierdlem64  46616  fourierdlem76  46628  fourierdlem102  46654  fourierdlem103  46655  fourierdlem104  46656  fourierdlem114  46666  meadjiunlem  46911  meaiininclem  46932  ovnsupge0  47003  hoidmvlelem2  47042  hoidmvlelem4  47044  vonvolmbllem  47106  vonvolmbl2  47109  vonvol2  47110  vonioolem1  47126  preimageiingt  47166  issmflem  47173  fsupdm  47288  finfdm  47292  fundcmpsurinjimaid  47883  perfectALTVlem2  48210  isubgruhgr  48356  uspgropssxp  48632  rhmsubcALTVlem4  48772  srhmsubcALTV  48813  imasubc  49638  imassc  49640  setrec2fun  50179  onsetreclem2  50193