Theorem eqsstrid 4043

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

Syntax hints:   → wi 4   = wceq 1536   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1776  df-cleq 2726  df-ss 3979

This theorem is referenced by:  eqsstrrid  4044  inss  4254  tpssi  4842  opabssxpd  5735  xpsspw  5821  fun  6770  fmpt  7129  fssrescdmd  7145  fliftrel  7327  knatar  7376  fr3nr  7790  ordsuci  7827  sucexeloniOLD  7829  suceloniOLD  7831  fiun  7965  f1iun  7966  1stcof  8042  2ndcof  8043  fsplitfpar  8141  fnwelem  8154  oeeui  8638  cofon1  8708  aceq3lem  10157  cflecard  10290  cfslb2n  10305  itunitc1  10457  axdc3lem2  10488  fpwwe2lem11  10678  canthwelem  10687  wuncval2  10784  peano5nni  12266  un0addcl  12556  un0mulcl  12557  fsuppmapnn0fiublem  14027  fsuppmapnn0fiub  14028  mertenslem2  15917  4sqlem11  16988  4sqlem19  16996  vdwlem13  17026  imasless  17586  rescfth  17990  oppchofcl  18316  oyoncl  18326  mgmidsssn0  18697  eqg0subg  19226  cycsubm  19232  efgsfo  19771  efgcpbllemb  19787  frgpuplem  19804  gsummpt1n0  19997  dprdfid  20051  dprd2d2  20078  ablfacrp  20100  ablfac1b  20104  ablfac1eu  20107  pgpfac1lem5  20113  ablfaclem3  20121  funcrngcsetc  20656  funcringcsetc  20690  srhmsubc  20696  rhmsubclem3  20703  lsptpcl  20994  lsppratlem3  21168  lsppratlem4  21169  lbsextlem2  21178  f1lindf  21859  topsn  22952  ordtbaslem  23211  ordtuni  23213  ordtbas2  23214  cnpco  23290  cnconst2  23306  tgcmp  23424  iunconn  23451  ptuni2  23599  xkococnlem  23682  tgqtop  23735  fbasrn  23907  uzrest  23920  fmco  23984  alexsubALT  24074  cnextf  24089  snclseqg  24139  ustund  24245  imasdsf1olem  24398  xmetresbl  24462  blsscls2  24532  metustss  24579  tngtopn  24686  reconn  24863  metnrmlem3  24896  cphsubrglem  25224  minveclem1  25471  minveclem3b  25475  ovolficcss  25517  ovolicc2lem4  25568  iundisj2  25597  uniioombllem4  25634  vitalilem5  25660  mbfeqalem1  25689  itg1addlem4  25747  itg1addlem4OLD  25748  limciun  25943  dvlip2  26048  dv11cn  26054  aalioulem3  26390  pserdvlem2  26486  pserdv  26487  abelthlem2  26490  efif1o  26602  efrlim  27026  efrlimOLD  27027  lgamgulmlem1  27086  fsumdvdsmul  27252  fsumdvdsmulOLD  27254  perfectlem2  27288  noextendseq  27726  nosupno  27762  nosupbnd2lem1  27774  noinfno  27777  noetasuplem4  27795  cuteq1  27892  addsbday  28064  setsvtx  29066  uhgredgn0  29159  upgredgss  29163  umgredgss  29164  usgredgss  29190  umgrres1lem  29341  upgrres1  29344  1hegrvtxdg1r  29540  clwlknf1oclwwlknlem3  30111  minvecolem1  30902  sh0le  31468  mdslmd3i  32360  iundisj2f  32609  suppss2f  32654  2ndresdju  32665  fnpreimac  32687  fdifsuppconst  32703  suppss3  32741  iundisj2fi  32804  erlval  33244  lsmsnorb  33398  pstmfval  33856  ordtrest2NEW  33883  ldgenpisyslem1  34143  ldgenpisyslem2  34144  omsmeas  34304  sitgclbn  34324  eulerpartlemt  34352  eulerpartlemmf  34356  eulerpartlemgf  34360  bnj849  34917  bnj1136  34989  bnj1311  35016  bnj1413  35027  bnj1452  35044  blsconn  35228  cvmliftlem2  35270  cvmlift2lem12  35298  mvtss  35537  mthmpps  35566  ellcsrspsn  35625  neibastop2lem  36342  filnetlem3  36362  finxpsuclem  37379  poimirlem3  37609  mblfinlem3  37645  areacirclem2  37695  sdclem1  37729  istotbnd3  37757  sstotbnd  37761  iccbnd  37826  icccmpALT  37827  osumcllem1N  39938  osumcllem2N  39939  osumcllem4N  39941  osumcllem9N  39946  pexmidlem6N  39957  dihglblem3N  41277  dvhdimlem  41426  dochexmidlem6  41447  lcfrlem16  41540  lcfr  41567  aks6d1c6lem3  42153  rhmqusspan  42166  ssabdv  42237  hbtlem6  43117  iocinico  43200  oege2  43296  omabs2  43321  tfsconcatb0  43333  trclubgNEW  43607  cnvrcl0  43614  relexp0a  43705  brtrclfv2  43716  cotrclrcl  43731  frege77d  43735  unhe1  43774  ntrrn  44111  imo72b2lem2  44156  imo72b2  44161  mnuprdlem4  44270  radcnvrat  44309  iunconnlem2  44932  ssinss2d  44999  limccog  45575  limsupresico  45655  liminfresico  45726  icccncfext  45842  stoweidlem14  45969  fourierdlem20  46082  fourierdlem42  46104  fourierdlem46  46107  fourierdlem50  46111  fourierdlem51  46112  fourierdlem54  46115  fourierdlem64  46125  fourierdlem76  46137  fourierdlem102  46163  fourierdlem103  46164  fourierdlem104  46165  fourierdlem114  46175  meadjiunlem  46420  meaiininclem  46441  ovnsupge0  46512  hoidmvlelem2  46551  hoidmvlelem4  46553  vonvolmbllem  46615  vonvolmbl2  46618  vonvol2  46619  vonioolem1  46635  issmflem  46682  fsupdm  46797  finfdm  46801  fundcmpsurinjimaid  47335  perfectALTVlem2  47646  isubgruhgr  47791  uspgropssxp  47987  rhmsubcALTVlem4  48127  srhmsubcALTV  48168  setrec2fun  48922  onsetreclem2  48936