Theorem eqsstrid 3946

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569   ⊆ wss 3895

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1812  df-cleq 2752  df-ss 3896

This theorem is used by:  eqsstrrid  3947  3sstr4g  3961  inss  4145  tpssi  4792  opabssxpd  5697  xpsspw  5786  fun  6745  fmpt  7111  fssrescdmd  7128  fliftrel  7317  knatar  7368  fr3nr  7787  ordsuci  7823  fiun  7956  f1iun  7957  1stcof  8032  2ndcof  8033  fsplitfpar  8132  fnwelem  8146  oeeui  8615  cofon1  8685  setrec2fun  9977  aceq3lem  10203  cflecard  10334  cfslb2n  10350  itunitc1  10502  axdc2lem  10530  axdc3lem2  10533  fpwwe2lem11  10730  canthwelem  10739  wuncval2  10836  peano5nni  12342  un0addcl  12643  un0mulcl  12644  fsuppmapnn0fiublem  14137  fsuppmapnn0fiub  14138  mertenslem2  16060  4sqlem11  17139  4sqlem19  17147  vdwlem13  17177  imasless  17718  rescfth  18120  oppchofcl  18440  oyoncl  18450  mgmidsssn0  18859  eqg0subg  19417  cycsubm  19423  efgsfo  19959  efgcpbllemb  19975  frgpuplem  19992  gsummpt1n0  20185  dprdfid  20239  dprd2d2  20266  ablfacrp  20288  ablfac1b  20292  ablfac1eu  20295  pgpfac1lem5  20301  ablfaclem3  20309  funcrngcsetc  20898  funcringcsetc  20932  srhmsubc  20938  rhmsubclem3  20945  lsptpcl  21260  lsppratlem3  21433  lsppratlem4  21434  lbsextlem2  21443  f1lindf  22134  topsn  23255  ordtbaslem  23512  ordtuni  23514  ordtbas2  23515  cnpco  23591  cnconst2  23607  tgcmp  23725  iunconn  23752  ptuni2  23901  xkococnlem  23984  tgqtop  24037  fbasrn  24209  uzrest  24222  fmco  24286  alexsubALT  24376  cnextf  24391  snclseqg  24441  ustund  24547  imasdsf1olem  24698  xmetresbl  24762  blsscls2  24829  metustss  24876  tngtopn  24975  reconn  25154  metnrmlem3  25187  cphsubrglem  25504  minveclem1  25751  minveclem3b  25755  ovolficcss  25796  ovolicc2lem4  25847  iundisj2  25876  uniioombllem4  25913  vitalilem5  25939  mbfeqalem1  25968  itg1addlem4  26026  limciun  26220  dvlip2  26321  dv11cn  26327  aalioulem3  26667  pserdvlem2  26761  pserdv  26762  abelthlem2  26765  efif1o  26880  efrlim  27303  lgamgulmlem1  27362  fsumdvdsmul  27528  perfectlem2  27563  noextendseq  28030  nosupno  28066  nosupbnd2lem1  28078  noinfno  28081  noetasuplem4  28099  cuteq1  28209  bdayiun  28307  addbday  28410  oncutlt  28656  oniso  28663  addonbday  28671  bdayn0p1  28761  bdaypw2n0bndlem  28855  setsvtx  29619  uhgredgn0  29712  upgredgss  29716  umgredgss  29717  usgredgss  29746  umgrres1lem  29897  upgrres1  29900  1hegrvtxdg1r  30095  clwlknf1oclwwlknlem3  30680  minvecolem1  31482  sh0le  32048  mdslmd3i  32940  iundisj2f  33232  suppss2f  33280  2ndresdju  33291  fnpreimac  33312  fdifsuppconst  33330  suppss3  33362  iundisj2fi  33436  elrgspnsubrunlem1  33855  erlval  33866  lsmsnorb  33993  extvfvvcl  34214  extvfvcl  34215  esplyind  34254  esplyindfv  34255  esplyfvn  34256  constrextdg2lem  34427  pstmfval  34575  ordtrest2NEW  34602  ldgenpisyslem1  34843  ldgenpisyslem2  34844  omsmeas  35002  sitgclbn  35022  eulerpartlemt  35050  eulerpartlemmf  35054  eulerpartlemgf  35058  bnj849  35602  bnj1136  35674  bnj1311  35701  bnj1413  35712  bnj1452  35729  kardnnfi  35894  rankkardu  35896  vonf1oonfo  35969  blsconn  36096  cvmliftlem2  36138  cvmlift2lem12  36166  mvtss  36405  mthmpps  36434  ellcsrspsn  36493  neibastop2lem  37241  filnetlem3  37261  ttcmin  37377  finxpsuclem  38414  poimirlem3  38635  mblfinlem3  38671  areacirclem2  38721  dfprop2  38740  sdclem1  38771  istotbnd3  38799  sstotbnd  38803  iccbnd  38868  icccmpALT  38869  osumcllem1N  41107  osumcllem2N  41108  osumcllem4N  41110  osumcllem9N  41115  pexmidlem6N  41126  dihglblem3N  42446  dvhdimlem  42595  dochexmidlem6  42616  lcfrlem16  42709  lcfr  42736  aks6d1c6lem3  43316  rhmqusspan  43329  ssabdv  43368  hbtlem6  44225  iocinico  44308  oege2  44403  omabs2  44428  tfsconcatb0  44440  trclubgNEW  44712  cnvrcl0  44719  relexp0a  44810  brtrclfv2  44821  cotrclrcl  44836  frege77d  44840  unhe1  44879  ntrrn  45216  imo72b2lem2  45261  imo72b2  45266  mnuprdlem4  45353  radcnvrat  45392  iunconnlem2  46011  ssinss2d  46171  limccog  46726  limsupresico  46804  liminfresico  46875  icccncfext  46991  stoweidlem14  47118  fourierdlem20  47231  fourierdlem42  47253  fourierdlem46  47256  fourierdlem50  47260  fourierdlem51  47261  fourierdlem54  47264  fourierdlem64  47274  fourierdlem76  47286  fourierdlem102  47312  fourierdlem103  47313  fourierdlem104  47314  fourierdlem114  47324  meadjiunlem  47569  meaiininclem  47590  ovnsupge0  47661  hoidmvlelem2  47700  hoidmvlelem4  47702  vonvolmbllem  47764  vonvolmbl2  47767  vonvol2  47768  vonioolem1  47784  preimageiingt  47824  issmflem  47831  fsupdm  47946  finfdm  47950  fundcmpsurinjimaid  48587  perfectALTVlem2  48914  isubgruhgr  49060  uspgropssxp  49336  rhmsubcALTVlem4  49475  srhmsubcALTV  49516  imasubc  50361  imassc  50363  onsetreclem2  50968