Theorem eqsstrid 4030

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-v 3475  df-in 3955  df-ss 3965

This theorem is referenced by:  eqsstrrid  4031  inss  4238  tpssi  4839  opabssxpd  5723  xpsspw  5809  fun  6753  fmpt  7111  fliftrel  7308  knatar  7357  fr3nr  7762  ordsuci  7799  sucexeloniOLD  7801  suceloniOLD  7803  fiun  7932  f1iun  7933  1stcof  8008  2ndcof  8009  fsplitfpar  8107  fnwelem  8120  oeeui  8605  cofon1  8674  aceq3lem  10118  cflecard  10251  cfslb2n  10266  itunitc1  10418  axdc3lem2  10449  fpwwe2lem11  10639  canthwelem  10648  wuncval2  10745  peano5nni  12220  un0addcl  12510  un0mulcl  12511  fsuppmapnn0fiublem  13960  fsuppmapnn0fiub  13961  mertenslem2  15836  4sqlem11  16893  4sqlem19  16901  vdwlem13  16931  imasless  17491  rescfth  17893  oppchofcl  18218  oyoncl  18228  mgmidsssn0  18598  eqg0subg  19112  cycsubm  19118  efgsfo  19649  efgcpbllemb  19665  frgpuplem  19682  gsummpt1n0  19875  dprdfid  19929  dprd2d2  19956  ablfacrp  19978  ablfac1b  19982  ablfac1eu  19985  pgpfac1lem5  19991  ablfaclem3  19999  lsptpcl  20735  lsppratlem3  20908  lsppratlem4  20909  lbsextlem2  20918  f1lindf  21597  topsn  22654  ordtbaslem  22913  ordtuni  22915  ordtbas2  22916  cnpco  22992  cnconst2  23008  tgcmp  23126  iunconn  23153  ptuni2  23301  xkococnlem  23384  tgqtop  23437  fbasrn  23609  uzrest  23622  fmco  23686  alexsubALT  23776  cnextf  23791  snclseqg  23841  ustund  23947  imasdsf1olem  24100  xmetresbl  24164  blsscls2  24234  metustss  24281  tngtopn  24388  reconn  24565  metnrmlem3  24598  cphsubrglem  24926  minveclem1  25173  minveclem3b  25177  ovolficcss  25219  ovolicc2lem4  25270  iundisj2  25299  uniioombllem4  25336  vitalilem5  25362  mbfeqalem1  25391  itg1addlem4  25449  itg1addlem4OLD  25450  limciun  25644  dvlip2  25748  dv11cn  25754  aalioulem3  26084  pserdvlem2  26177  pserdv  26178  abelthlem2  26181  efif1o  26292  efrlim  26711  lgamgulmlem1  26770  fsumdvdsmul  26936  perfectlem2  26970  noextendseq  27407  nosupno  27443  nosupbnd2lem1  27455  noinfno  27458  noetasuplem4  27476  cuteq1  27572  peano5n0s  27936  setsvtx  28563  uhgredgn0  28656  upgredgss  28660  umgredgss  28661  usgredgss  28687  umgrres1lem  28835  upgrres1  28838  1hegrvtxdg1r  29033  clwlknf1oclwwlknlem3  29604  minvecolem1  30395  sh0le  30961  mdslmd3i  31853  iundisj2f  32089  suppss2f  32131  2ndresdju  32142  fnpreimac  32164  fdifsuppconst  32179  suppss3  32217  iundisj2fi  32276  lsmsnorb  32776  pstmfval  33175  ordtrest2NEW  33202  ldgenpisyslem1  33460  ldgenpisyslem2  33461  omsmeas  33621  sitgclbn  33641  eulerpartlemt  33669  eulerpartlemmf  33673  eulerpartlemgf  33677  bnj849  34235  bnj1136  34307  bnj1311  34334  bnj1413  34345  bnj1452  34362  blsconn  34534  cvmliftlem2  34576  cvmlift2lem12  34604  mvtss  34843  mthmpps  34872  neibastop2lem  35549  filnetlem3  35569  finxpsuclem  36582  poimirlem3  36795  mblfinlem3  36831  areacirclem2  36881  sdclem1  36915  istotbnd3  36943  sstotbnd  36947  iccbnd  37012  icccmpALT  37013  osumcllem1N  39131  osumcllem2N  39132  osumcllem4N  39134  osumcllem9N  39139  pexmidlem6N  39150  dihglblem3N  40470  dvhdimlem  40619  dochexmidlem6  40640  lcfrlem16  40733  lcfr  40760  ssabdv  41344  hbtlem6  42174  iocinico  42264  oege2  42360  omabs2  42385  tfsconcatb0  42397  trclubgNEW  42672  cnvrcl0  42679  relexp0a  42770  brtrclfv2  42781  cotrclrcl  42796  frege77d  42800  unhe1  42839  ntrrn  43176  imo72b2lem0  43220  imo72b2lem2  43222  imo72b2  43227  mnuprdlem4  43337  radcnvrat  43376  iunconnlem2  43999  ssinss2d  44049  limccog  44635  limsupresico  44715  liminfresico  44786  icccncfext  44902  stoweidlem14  45029  fourierdlem20  45142  fourierdlem42  45164  fourierdlem46  45167  fourierdlem50  45171  fourierdlem51  45172  fourierdlem54  45175  fourierdlem64  45185  fourierdlem76  45197  fourierdlem102  45223  fourierdlem103  45224  fourierdlem104  45225  fourierdlem114  45235  meadjiunlem  45480  meaiininclem  45501  ovnsupge0  45572  hoidmvlelem2  45611  hoidmvlelem4  45613  vonvolmbllem  45675  vonvolmbl2  45678  vonvol2  45679  vonioolem1  45695  issmflem  45742  fsupdm  45857  finfdm  45861  fundcmpsurinjimaid  46378  perfectALTVlem2  46689  uspgropssxp  46821  funcrngcsetc  46985  funcringcsetc  47022  srhmsubc  47063  rhmsubclem3  47075  srhmsubcALTV  47081  rhmsubcALTVlem4  47094  setrec2fun  47825  onsetreclem2  47839