Theorem eqsstrid 3965

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

Syntax hints:   → wi 4   = wceq 1539   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890  df-ss 3900

This theorem is referenced by:  eqsstrrid  3966  inss  4169  tpssi  4766  opabssxpd  5625  xpsspw  5708  fun  6620  fmpt  6966  fliftrel  7159  knatar  7208  fr3nr  7600  suceloni  7635  fiun  7759  f1iun  7760  1stcof  7834  2ndcof  7835  fsplitfpar  7930  fnwelem  7943  oeeui  8395  trpredss  9407  trpredmintr  9409  aceq3lem  9807  cflecard  9940  cfslb2n  9955  itunitc1  10107  axdc3lem2  10138  fpwwe2lem11  10328  canthwelem  10337  wuncval2  10434  peano5nni  11906  un0addcl  12196  un0mulcl  12197  fsuppmapnn0fiublem  13638  fsuppmapnn0fiub  13639  mertenslem2  15525  4sqlem11  16584  4sqlem19  16592  vdwlem13  16622  imasless  17168  rescfth  17569  oppchofcl  17894  oyoncl  17904  mgmidsssn0  18271  cycsubm  18736  efgsfo  19260  efgcpbllemb  19276  frgpuplem  19293  gsummpt1n0  19481  dprdfid  19535  dprd2d2  19562  ablfacrp  19584  ablfac1b  19588  ablfac1eu  19591  pgpfac1lem5  19597  ablfaclem3  19605  lsptpcl  20156  lsppratlem3  20326  lsppratlem4  20327  lbsextlem2  20336  f1lindf  20939  topsn  21988  ordtbaslem  22247  ordtuni  22249  ordtbas2  22250  cnpco  22326  cnconst2  22342  tgcmp  22460  iunconn  22487  ptuni2  22635  xkococnlem  22718  tgqtop  22771  fbasrn  22943  uzrest  22956  fmco  23020  alexsubALT  23110  cnextf  23125  snclseqg  23175  ustund  23281  imasdsf1olem  23434  xmetresbl  23498  blsscls2  23566  metustss  23613  tngtopn  23720  reconn  23897  metnrmlem3  23930  cphsubrglem  24246  minveclem1  24493  minveclem3b  24497  ovolficcss  24538  ovolicc2lem4  24589  iundisj2  24618  uniioombllem4  24655  vitalilem5  24681  mbfeqalem1  24710  itg1addlem4  24768  itg1addlem4OLD  24769  limciun  24963  dvlip2  25064  dv11cn  25070  aalioulem3  25399  pserdvlem2  25492  pserdv  25493  abelthlem2  25496  efif1o  25607  efrlim  26024  lgamgulmlem1  26083  fsumdvdsmul  26249  perfectlem2  26283  setsvtx  27308  uhgredgn0  27401  upgredgss  27405  umgredgss  27406  usgredgss  27432  umgrres1lem  27580  upgrres1  27583  1hegrvtxdg1r  27778  clwlknf1oclwwlknlem3  28348  minvecolem1  29137  sh0le  29703  mdslmd3i  30595  iundisj2f  30830  suppss2f  30875  2ndresdju  30887  fnpreimac  30910  fdifsuppconst  30925  suppss3  30961  iundisj2fi  31020  lsmsnorb  31481  pstmfval  31748  ordtrest2NEW  31775  ldgenpisyslem1  32031  ldgenpisyslem2  32032  omsmeas  32190  sitgclbn  32210  eulerpartlemt  32238  eulerpartlemmf  32242  eulerpartlemgf  32246  bnj849  32805  bnj1136  32877  bnj1311  32904  bnj1413  32915  bnj1452  32932  blsconn  33106  cvmliftlem2  33148  cvmlift2lem12  33176  mvtss  33415  mthmpps  33444  noextendseq  33797  nosupno  33833  nosupbnd2lem1  33845  noinfno  33848  noetasuplem4  33866  neibastop2lem  34476  filnetlem3  34496  finxpsuclem  35495  poimirlem3  35707  mblfinlem3  35743  areacirclem2  35793  sdclem1  35828  istotbnd3  35856  sstotbnd  35860  iccbnd  35925  icccmpALT  35926  osumcllem1N  37897  osumcllem2N  37898  osumcllem4N  37900  osumcllem9N  37905  pexmidlem6N  37916  dihglblem3N  39236  dvhdimlem  39385  dochexmidlem6  39406  lcfrlem16  39499  lcfr  39526  hbtlem6  40870  iocinico  40959  trclubgNEW  41115  cnvrcl0  41122  relexp0a  41213  brtrclfv2  41224  cotrclrcl  41239  frege77d  41243  unhe1  41282  ntrrn  41621  imo72b2lem0  41665  imo72b2lem2  41667  imo72b2  41672  mnuprdlem4  41782  radcnvrat  41821  iunconnlem2  42444  ssinss2d  42497  limccog  43051  limsupresico  43131  liminfresico  43202  icccncfext  43318  stoweidlem14  43445  fourierdlem20  43558  fourierdlem42  43580  fourierdlem46  43583  fourierdlem50  43587  fourierdlem51  43588  fourierdlem54  43591  fourierdlem64  43601  fourierdlem76  43613  fourierdlem102  43639  fourierdlem103  43640  fourierdlem104  43641  fourierdlem114  43651  meadjiunlem  43893  meaiininclem  43914  ovnsupge0  43985  hoidmvlelem2  44024  hoidmvlelem4  44026  vonvolmbllem  44088  vonvolmbl2  44091  vonvol2  44092  vonioolem1  44108  issmflem  44150  fundcmpsurinjimaid  44751  perfectALTVlem2  45062  uspgropssxp  45194  funcrngcsetc  45444  funcringcsetc  45481  srhmsubc  45522  rhmsubclem3  45534  srhmsubcALTV  45540  rhmsubcALTVlem4  45553  setrec2fun  46284  onsetreclem2  46297