Theorem eqsstrid 3969

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

This proof depends on syntax axioms:   → wi 4   = wceq 1570   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2155  ax-ext 2732

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

This theorem is used by:  eqsstrrid  3970  3sstr4g  3984  inss  4194  tpssi  4798  opabssxpd  5702  xpsspw  5790  fun  6737  fmpt  7103  fssrescdmd  7120  fliftrel  7309  knatar  7360  fr3nr  7771  ordsuci  7807  fiun  7940  f1iun  7941  1stcof  8016  2ndcof  8017  fsplitfpar  8115  fnwelem  8129  oeeui  8590  cofon1  8660  aceq3lem  10123  cflecard  10254  cfslb2n  10270  itunitc1  10422  axdc2lem  10450  axdc3lem2  10453  fpwwe2lem11  10650  canthwelem  10659  wuncval2  10756  peano5nni  12260  un0addcl  12561  un0mulcl  12562  fsuppmapnn0fiublem  14054  fsuppmapnn0fiub  14055  mertenslem2  15974  4sqlem11  17047  4sqlem19  17055  vdwlem13  17085  imasless  17626  rescfth  18028  oppchofcl  18348  oyoncl  18358  mgmidsssn0  18766  eqg0subg  19324  cycsubm  19330  efgsfo  19866  efgcpbllemb  19882  frgpuplem  19899  gsummpt1n0  20092  dprdfid  20146  dprd2d2  20173  ablfacrp  20195  ablfac1b  20199  ablfac1eu  20202  pgpfac1lem5  20208  ablfaclem3  20216  funcrngcsetc  20802  funcringcsetc  20836  srhmsubc  20842  rhmsubclem3  20849  lsptpcl  21163  lsppratlem3  21336  lsppratlem4  21337  lbsextlem2  21346  f1lindf  22035  topsn  23156  ordtbaslem  23413  ordtuni  23415  ordtbas2  23416  cnpco  23492  cnconst2  23508  tgcmp  23626  iunconn  23653  ptuni2  23802  xkococnlem  23885  tgqtop  23938  fbasrn  24110  uzrest  24123  fmco  24187  alexsubALT  24277  cnextf  24292  snclseqg  24342  ustund  24448  imasdsf1olem  24599  xmetresbl  24663  blsscls2  24730  metustss  24777  tngtopn  24876  reconn  25055  metnrmlem3  25088  cphsubrglem  25405  minveclem1  25652  minveclem3b  25656  ovolficcss  25697  ovolicc2lem4  25748  iundisj2  25777  uniioombllem4  25814  vitalilem5  25840  mbfeqalem1  25869  itg1addlem4  25927  limciun  26121  dvlip2  26222  dv11cn  26228  aalioulem3  26570  pserdvlem2  26664  pserdv  26665  abelthlem2  26668  efif1o  26783  efrlim  27206  lgamgulmlem1  27265  fsumdvdsmul  27431  perfectlem2  27466  noextendseq  27903  nosupno  27939  nosupbnd2lem1  27951  noinfno  27954  noetasuplem4  27972  cuteq1  28082  bdayiun  28180  addbday  28283  oncutlt  28529  oniso  28536  addonbday  28544  bdayn0p1  28634  bdaypw2n0bndlem  28728  setsvtx  29492  uhgredgn0  29585  upgredgss  29589  umgredgss  29590  usgredgss  29619  umgrres1lem  29770  upgrres1  29773  1hegrvtxdg1r  29968  clwlknf1oclwwlknlem3  30553  minvecolem1  31355  sh0le  31921  mdslmd3i  32813  iundisj2f  33063  suppss2f  33111  2ndresdju  33122  fnpreimac  33143  fdifsuppconst  33161  suppss3  33194  iundisj2fi  33268  elrgspnsubrunlem1  33687  erlval  33698  lsmsnorb  33824  extvfvvcl  34045  extvfvcl  34046  esplyind  34085  esplyindfv  34086  esplyfvn  34087  constrextdg2lem  34258  pstmfval  34406  ordtrest2NEW  34433  ldgenpisyslem1  34674  ldgenpisyslem2  34675  omsmeas  34834  sitgclbn  34854  eulerpartlemt  34882  eulerpartlemmf  34886  eulerpartlemgf  34890  bnj849  35434  bnj1136  35506  bnj1311  35533  bnj1413  35544  bnj1452  35561  kardnnfi  35695  rankkardu  35697  vonf1oonfo  35712  blsconn  35823  cvmliftlem2  35865  cvmlift2lem12  35893  mvtss  36132  mthmpps  36161  ellcsrspsn  36220  neibastop2lem  36979  filnetlem3  36999  ttcmin  37115  finxpsuclem  38151  poimirlem3  38372  mblfinlem3  38408  areacirclem2  38458  sdclem1  38493  istotbnd3  38521  sstotbnd  38525  iccbnd  38590  icccmpALT  38591  osumcllem1N  40829  osumcllem2N  40830  osumcllem4N  40832  osumcllem9N  40837  pexmidlem6N  40848  dihglblem3N  42168  dvhdimlem  42317  dochexmidlem6  42338  lcfrlem16  42431  lcfr  42458  aks6d1c6lem3  43038  rhmqusspan  43051  ssabdv  43090  hbtlem6  43970  iocinico  44053  oege2  44148  omabs2  44173  tfsconcatb0  44185  trclubgNEW  44458  cnvrcl0  44465  relexp0a  44556  brtrclfv2  44567  cotrclrcl  44582  frege77d  44586  unhe1  44625  ntrrn  44962  imo72b2lem2  45007  imo72b2  45012  mnuprdlem4  45099  radcnvrat  45138  iunconnlem2  45757  ssinss2d  45894  limccog  46450  limsupresico  46528  liminfresico  46599  icccncfext  46715  stoweidlem14  46842  fourierdlem20  46955  fourierdlem42  46977  fourierdlem46  46980  fourierdlem50  46984  fourierdlem51  46985  fourierdlem54  46988  fourierdlem64  46998  fourierdlem76  47010  fourierdlem102  47036  fourierdlem103  47037  fourierdlem104  47038  fourierdlem114  47048  meadjiunlem  47293  meaiininclem  47314  ovnsupge0  47385  hoidmvlelem2  47424  hoidmvlelem4  47426  vonvolmbllem  47488  vonvolmbl2  47491  vonvol2  47492  vonioolem1  47508  preimageiingt  47548  issmflem  47555  fsupdm  47670  finfdm  47674  fundcmpsurinjimaid  48311  perfectALTVlem2  48638  isubgruhgr  48784  uspgropssxp  49060  rhmsubcALTVlem4  49199  srhmsubcALTV  49240  imasubc  50077  imassc  50079  setrec2fun  50618  onsetreclem2  50632