Theorem eqsstrid 4015

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3936

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 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-in 3943  df-ss 3952

This theorem is referenced by:  eqsstrrid  4016  inss  4215  tpssi  4769  xpsspw  5682  opabssxpd  5789  fun  6540  fmpt  6874  fliftrel  7061  knatar  7110  fr3nr  7494  suceloni  7528  fiun  7644  f1iun  7645  1stcof  7719  2ndcof  7720  fsplitfpar  7814  fnwelem  7825  oeeui  8228  aceq3lem  9546  cflecard  9675  cfslb2n  9690  itunitc1  9842  axdc3lem2  9873  fpwwe2lem12  10063  canthwelem  10072  wuncval2  10169  peano5nni  11641  un0addcl  11931  un0mulcl  11932  fsuppmapnn0fiublem  13359  fsuppmapnn0fiub  13360  mertenslem2  15241  4sqlem11  16291  4sqlem19  16299  vdwlem13  16329  imasless  16813  rescfth  17207  oppchofcl  17510  oyoncl  17520  mgmidsssn0  17882  cycsubm  18345  efgsfo  18865  efgcpbllemb  18881  frgpuplem  18898  gsummpt1n0  19085  dprdfid  19139  dprd2d2  19166  ablfacrp  19188  ablfac1b  19192  ablfac1eu  19195  pgpfac1lem5  19201  ablfaclem3  19209  lsptpcl  19751  lsppratlem3  19921  lsppratlem4  19922  lbsextlem2  19931  f1lindf  20966  topsn  21539  ordtbaslem  21796  ordtuni  21798  ordtbas2  21799  cnpco  21875  cnconst2  21891  tgcmp  22009  iunconn  22036  ptuni2  22184  xkococnlem  22267  tgqtop  22320  fbasrn  22492  uzrest  22505  fmco  22569  alexsubALT  22659  cnextf  22674  snclseqg  22724  ustund  22830  imasdsf1olem  22983  xmetresbl  23047  blsscls2  23114  metustss  23161  tngtopn  23259  reconn  23436  metnrmlem3  23469  cphsubrglem  23781  minveclem1  24027  minveclem3b  24031  ovolficcss  24070  ovolicc2lem4  24121  iundisj2  24150  uniioombllem4  24187  vitalilem5  24213  mbfeqalem1  24242  itg1addlem4  24300  limciun  24492  dvlip2  24592  dv11cn  24598  aalioulem3  24923  pserdvlem2  25016  pserdv  25017  abelthlem2  25020  efif1o  25130  efrlim  25547  lgamgulmlem1  25606  fsumdvdsmul  25772  perfectlem2  25806  setsvtx  26820  uhgredgn0  26913  upgredgss  26917  umgredgss  26918  usgredgss  26944  umgrres1lem  27092  upgrres1  27095  1hegrvtxdg1r  27290  clwlknf1oclwwlknlem3  27862  minvecolem1  28651  sh0le  29217  mdslmd3i  30109  iundisj2f  30340  suppss2f  30384  fnpreimac  30416  suppss3  30460  iundisj2fi  30520  lsmsnorb  30945  pstmfval  31136  ordtrest2NEW  31166  ldgenpisyslem1  31422  ldgenpisyslem2  31423  omsmeas  31581  sitgclbn  31601  eulerpartlemt  31629  eulerpartlemmf  31633  eulerpartlemgf  31637  bnj849  32197  bnj1136  32269  bnj1311  32296  bnj1413  32307  bnj1452  32324  blsconn  32491  cvmliftlem2  32533  cvmlift2lem12  32561  mvtss  32800  mthmpps  32829  trpredss  33068  trpredmintr  33070  noextendseq  33174  nosupno  33203  nosupbnd2lem1  33215  noetalem3  33219  neibastop2lem  33708  filnetlem3  33728  finxpsuclem  34681  poimirlem3  34910  mblfinlem3  34946  areacirclem2  34998  sdclem1  35033  istotbnd3  35064  sstotbnd  35068  iccbnd  35133  icccmpALT  35134  osumcllem1N  37107  osumcllem2N  37108  osumcllem4N  37110  osumcllem9N  37115  pexmidlem6N  37126  dihglblem3N  38446  dvhdimlem  38595  dochexmidlem6  38616  lcfrlem16  38709  lcfr  38736  hbtlem6  39778  iocinico  39867  trclubgNEW  40027  cnvrcl0  40034  relexp0a  40110  brtrclfv2  40121  cotrclrcl  40136  frege77d  40140  unhe1  40180  ntrrn  40521  imo72b2lem0  40565  imo72b2lem2  40567  imo72b2  40574  mnuprdlem4  40660  radcnvrat  40695  iunconnlem2  41318  ssinss2d  41371  limccog  41950  limsupresico  42030  liminfresico  42101  icccncfext  42219  stoweidlem14  42348  fourierdlem20  42461  fourierdlem42  42483  fourierdlem46  42486  fourierdlem50  42490  fourierdlem51  42491  fourierdlem54  42494  fourierdlem64  42504  fourierdlem76  42516  fourierdlem102  42542  fourierdlem103  42543  fourierdlem104  42544  fourierdlem114  42554  meadjiunlem  42796  meaiininclem  42817  ovnsupge0  42888  hoidmvlelem2  42927  hoidmvlelem4  42929  vonvolmbllem  42991  vonvolmbl2  42994  vonvol2  42995  vonioolem1  43011  issmflem  43053  fundcmpsurinjimaid  43620  perfectALTVlem2  43936  uspgropssxp  44068  funcrngcsetc  44318  funcringcsetc  44355  srhmsubc  44396  rhmsubclem3  44408  srhmsubcALTV  44414  rhmsubcALTVlem4  44427  setrec2fun  44844  onsetreclem2  44857