Theorem eqsstrid 3963

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

Syntax hints:   → wi 4   = wceq 1538   ⊆ wss 3881

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-v 3443  df-in 3888  df-ss 3898

This theorem is referenced by:  eqsstrrid  3964  inss  4165  tpssi  4729  xpsspw  5646  opabssxpd  5753  fun  6514  fmpt  6851  fliftrel  7040  knatar  7089  fr3nr  7474  suceloni  7508  fiun  7626  f1iun  7627  1stcof  7701  2ndcof  7702  fsplitfpar  7797  fnwelem  7808  oeeui  8211  aceq3lem  9531  cflecard  9664  cfslb2n  9679  itunitc1  9831  axdc3lem2  9862  fpwwe2lem12  10052  canthwelem  10061  wuncval2  10158  peano5nni  11628  un0addcl  11918  un0mulcl  11919  fsuppmapnn0fiublem  13353  fsuppmapnn0fiub  13354  mertenslem2  15233  4sqlem11  16281  4sqlem19  16289  vdwlem13  16319  imasless  16805  rescfth  17199  oppchofcl  17502  oyoncl  17512  mgmidsssn0  17874  cycsubm  18337  efgsfo  18857  efgcpbllemb  18873  frgpuplem  18890  gsummpt1n0  19078  dprdfid  19132  dprd2d2  19159  ablfacrp  19181  ablfac1b  19185  ablfac1eu  19188  pgpfac1lem5  19194  ablfaclem3  19202  lsptpcl  19744  lsppratlem3  19914  lsppratlem4  19915  lbsextlem2  19924  f1lindf  20511  topsn  21536  ordtbaslem  21793  ordtuni  21795  ordtbas2  21796  cnpco  21872  cnconst2  21888  tgcmp  22006  iunconn  22033  ptuni2  22181  xkococnlem  22264  tgqtop  22317  fbasrn  22489  uzrest  22502  fmco  22566  alexsubALT  22656  cnextf  22671  snclseqg  22721  ustund  22827  imasdsf1olem  22980  xmetresbl  23044  blsscls2  23111  metustss  23158  tngtopn  23256  reconn  23433  metnrmlem3  23466  cphsubrglem  23782  minveclem1  24028  minveclem3b  24032  ovolficcss  24073  ovolicc2lem4  24124  iundisj2  24153  uniioombllem4  24190  vitalilem5  24216  mbfeqalem1  24245  itg1addlem4  24303  limciun  24497  dvlip2  24598  dv11cn  24604  aalioulem3  24930  pserdvlem2  25023  pserdv  25024  abelthlem2  25027  efif1o  25138  efrlim  25555  lgamgulmlem1  25614  fsumdvdsmul  25780  perfectlem2  25814  setsvtx  26828  uhgredgn0  26921  upgredgss  26925  umgredgss  26926  usgredgss  26952  umgrres1lem  27100  upgrres1  27103  1hegrvtxdg1r  27298  clwlknf1oclwwlknlem3  27868  minvecolem1  28657  sh0le  29223  mdslmd3i  30115  iundisj2f  30353  suppss2f  30398  2ndresdju  30411  fnpreimac  30434  fdifsuppconst  30449  suppss3  30486  iundisj2fi  30546  lsmsnorb  30999  pstmfval  31249  ordtrest2NEW  31276  ldgenpisyslem1  31532  ldgenpisyslem2  31533  omsmeas  31691  sitgclbn  31711  eulerpartlemt  31739  eulerpartlemmf  31743  eulerpartlemgf  31747  bnj849  32307  bnj1136  32379  bnj1311  32406  bnj1413  32417  bnj1452  32434  blsconn  32604  cvmliftlem2  32646  cvmlift2lem12  32674  mvtss  32913  mthmpps  32942  trpredss  33181  trpredmintr  33183  noextendseq  33287  nosupno  33316  nosupbnd2lem1  33328  noetalem3  33332  neibastop2lem  33821  filnetlem3  33841  finxpsuclem  34814  poimirlem3  35060  mblfinlem3  35096  areacirclem2  35146  sdclem1  35181  istotbnd3  35209  sstotbnd  35213  iccbnd  35278  icccmpALT  35279  osumcllem1N  37252  osumcllem2N  37253  osumcllem4N  37255  osumcllem9N  37260  pexmidlem6N  37271  dihglblem3N  38591  dvhdimlem  38740  dochexmidlem6  38761  lcfrlem16  38854  lcfr  38881  hbtlem6  40073  iocinico  40162  trclubgNEW  40318  cnvrcl0  40325  relexp0a  40417  brtrclfv2  40428  cotrclrcl  40443  frege77d  40447  unhe1  40486  ntrrn  40825  imo72b2lem0  40869  imo72b2lem2  40871  imo72b2  40878  mnuprdlem4  40983  radcnvrat  41018  iunconnlem2  41641  ssinss2d  41694  limccog  42262  limsupresico  42342  liminfresico  42413  icccncfext  42529  stoweidlem14  42656  fourierdlem20  42769  fourierdlem42  42791  fourierdlem46  42794  fourierdlem50  42798  fourierdlem51  42799  fourierdlem54  42802  fourierdlem64  42812  fourierdlem76  42824  fourierdlem102  42850  fourierdlem103  42851  fourierdlem104  42852  fourierdlem114  42862  meadjiunlem  43104  meaiininclem  43125  ovnsupge0  43196  hoidmvlelem2  43235  hoidmvlelem4  43237  vonvolmbllem  43299  vonvolmbl2  43302  vonvol2  43303  vonioolem1  43319  issmflem  43361  fundcmpsurinjimaid  43928  perfectALTVlem2  44240  uspgropssxp  44372  funcrngcsetc  44622  funcringcsetc  44659  srhmsubc  44700  rhmsubclem3  44712  srhmsubcALTV  44718  rhmsubcALTVlem4  44731  setrec2fun  45222  onsetreclem2  45235