Theorem eqsstrid 3953

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 235	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731  df-ss 3900

This theorem is referenced by:  eqsstrrid  3954  3sstr4g  3968  inss  4176  tpssi  4769  opabssxpd  5665  xpsspw  5752  fun  6689  fmpt  7051  fssrescdmd  7068  fliftrel  7252  knatar  7301  fr3nr  7715  ordsuci  7751  fiun  7885  f1iun  7886  1stcof  7961  2ndcof  7962  fsplitfpar  8057  fnwelem  8071  oeeui  8528  cofon1  8598  aceq3lem  10033  cflecard  10166  cfslb2n  10181  itunitc1  10333  axdc2lem  10361  axdc3lem2  10364  fpwwe2lem11  10555  canthwelem  10564  wuncval2  10661  peano5nni  12168  un0addcl  12461  un0mulcl  12462  fsuppmapnn0fiublem  13943  fsuppmapnn0fiub  13944  mertenslem2  15841  4sqlem11  16917  4sqlem19  16925  vdwlem13  16955  imasless  17495  rescfth  17897  oppchofcl  18217  oyoncl  18227  mgmidsssn0  18631  eqg0subg  19162  cycsubm  19168  efgsfo  19705  efgcpbllemb  19721  frgpuplem  19738  gsummpt1n0  19931  dprdfid  19985  dprd2d2  20012  ablfacrp  20034  ablfac1b  20038  ablfac1eu  20041  pgpfac1lem5  20047  ablfaclem3  20055  funcrngcsetc  20612  funcringcsetc  20646  srhmsubc  20652  rhmsubclem3  20659  lsptpcl  20969  lsppratlem3  21142  lsppratlem4  21143  lbsextlem2  21152  f1lindf  21797  topsn  22914  ordtbaslem  23171  ordtuni  23173  ordtbas2  23174  cnpco  23250  cnconst2  23266  tgcmp  23384  iunconn  23411  ptuni2  23559  xkococnlem  23642  tgqtop  23695  fbasrn  23867  uzrest  23880  fmco  23944  alexsubALT  24034  cnextf  24049  snclseqg  24099  ustund  24205  imasdsf1olem  24356  xmetresbl  24420  blsscls2  24487  metustss  24534  tngtopn  24633  reconn  24812  metnrmlem3  24845  cphsubrglem  25162  minveclem1  25409  minveclem3b  25413  ovolficcss  25454  ovolicc2lem4  25505  iundisj2  25534  uniioombllem4  25571  vitalilem5  25597  mbfeqalem1  25626  itg1addlem4  25684  limciun  25879  dvlip2  25980  dv11cn  25986  aalioulem3  26318  pserdvlem2  26411  pserdv  26412  abelthlem2  26415  efif1o  26528  efrlim  26951  lgamgulmlem1  27010  fsumdvdsmul  27176  perfectlem2  27211  noextendseq  27649  nosupno  27685  nosupbnd2lem1  27697  noinfno  27700  noetasuplem4  27718  cuteq1  27827  bdayiun  27925  addbday  28028  oncutlt  28274  oniso  28281  addonbday  28289  bdayn0p1  28379  bdaypw2n0bndlem  28473  setsvtx  29122  uhgredgn0  29215  upgredgss  29219  umgredgss  29220  usgredgss  29246  umgrres1lem  29397  upgrres1  29400  1hegrvtxdg1r  29595  clwlknf1oclwwlknlem3  30171  minvecolem1  30963  sh0le  31529  mdslmd3i  32421  iundisj2f  32679  suppss2f  32730  2ndresdju  32741  fnpreimac  32762  fdifsuppconst  32781  suppss3  32815  iundisj2fi  32889  elrgspnsubrunlem1  33328  erlval  33339  lsmsnorb  33474  extvfvvcl  33719  extvfvcl  33720  esplyind  33759  esplyindfv  33760  esplyfvn  33761  constrextdg2lem  33932  pstmfval  34080  ordtrest2NEW  34107  ldgenpisyslem1  34347  ldgenpisyslem2  34348  omsmeas  34507  sitgclbn  34527  eulerpartlemt  34555  eulerpartlemmf  34559  eulerpartlemgf  34563  bnj849  35107  bnj1136  35179  bnj1311  35206  bnj1413  35217  bnj1452  35234  blsconn  35472  cvmliftlem2  35514  cvmlift2lem12  35542  mvtss  35781  mthmpps  35810  ellcsrspsn  35869  neibastop2lem  36588  filnetlem3  36608  ttcmin  36724  finxpsuclem  37759  poimirlem3  37990  mblfinlem3  38026  areacirclem2  38076  sdclem1  38110  istotbnd3  38138  sstotbnd  38142  iccbnd  38207  icccmpALT  38208  osumcllem1N  40448  osumcllem2N  40449  osumcllem4N  40451  osumcllem9N  40456  pexmidlem6N  40467  dihglblem3N  41787  dvhdimlem  41936  dochexmidlem6  41957  lcfrlem16  42050  lcfr  42077  aks6d1c6lem3  42657  rhmqusspan  42670  ssabdv  42707  hbtlem6  43574  iocinico  43657  oege2  43752  omabs2  43777  tfsconcatb0  43789  trclubgNEW  44062  cnvrcl0  44069  relexp0a  44160  brtrclfv2  44171  cotrclrcl  44186  frege77d  44190  unhe1  44229  ntrrn  44566  imo72b2lem2  44611  imo72b2  44616  mnuprdlem4  44719  radcnvrat  44758  iunconnlem2  45378  ssinss2d  45508  limccog  46065  limsupresico  46143  liminfresico  46214  icccncfext  46330  stoweidlem14  46457  fourierdlem20  46570  fourierdlem42  46592  fourierdlem46  46595  fourierdlem50  46599  fourierdlem51  46600  fourierdlem54  46603  fourierdlem64  46613  fourierdlem76  46625  fourierdlem102  46651  fourierdlem103  46652  fourierdlem104  46653  fourierdlem114  46663  meadjiunlem  46908  meaiininclem  46929  ovnsupge0  47000  hoidmvlelem2  47039  hoidmvlelem4  47041  vonvolmbllem  47103  vonvolmbl2  47106  vonvol2  47107  vonioolem1  47123  preimageiingt  47163  issmflem  47170  fsupdm  47285  finfdm  47289  fundcmpsurinjimaid  47886  perfectALTVlem2  48213  isubgruhgr  48359  uspgropssxp  48635  rhmsubcALTVlem4  48775  srhmsubcALTV  48816  imasubc  49641  imassc  49643  setrec2fun  50182  onsetreclem2  50196