Theorem eqsstrid 3972

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

Syntax hints:   → wi 4   = wceq 1559   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-ex 1799  df-cleq 2753  df-ss 3919

This theorem is referenced by:  eqsstrrid  3973  3sstr4g  3987  inss  4198  tpssi  4793  opabssxpd  5690  xpsspw  5778  fun  6721  fmpt  7086  fssrescdmd  7103  fliftrel  7287  knatar  7336  fr3nr  7750  ordsuci  7786  fiun  7919  f1iun  7920  1stcof  7995  2ndcof  7996  fsplitfpar  8091  fnwelem  8105  oeeui  8566  cofon1  8636  aceq3lem  10070  cflecard  10203  cfslb2n  10219  itunitc1  10371  axdc2lem  10399  axdc3lem2  10402  fpwwe2lem11  10593  canthwelem  10602  wuncval2  10699  peano5nni  12207  un0addcl  12508  un0mulcl  12509  fsuppmapnn0fiublem  13997  fsuppmapnn0fiub  13998  mertenslem2  15906  4sqlem11  16982  4sqlem19  16990  vdwlem13  17020  imasless  17561  rescfth  17963  oppchofcl  18283  oyoncl  18293  mgmidsssn0  18697  eqg0subg  19228  cycsubm  19234  efgsfo  19770  efgcpbllemb  19786  frgpuplem  19803  gsummpt1n0  19996  dprdfid  20050  dprd2d2  20077  ablfacrp  20099  ablfac1b  20103  ablfac1eu  20106  pgpfac1lem5  20112  ablfaclem3  20120  funcrngcsetc  20677  funcringcsetc  20711  srhmsubc  20717  rhmsubclem3  20724  lsptpcl  21034  lsppratlem3  21207  lsppratlem4  21208  lbsextlem2  21217  f1lindf  21862  topsn  22979  ordtbaslem  23236  ordtuni  23238  ordtbas2  23239  cnpco  23315  cnconst2  23331  tgcmp  23449  iunconn  23476  ptuni2  23624  xkococnlem  23707  tgqtop  23760  fbasrn  23932  uzrest  23945  fmco  24009  alexsubALT  24099  cnextf  24114  snclseqg  24164  ustund  24270  imasdsf1olem  24421  xmetresbl  24485  blsscls2  24552  metustss  24599  tngtopn  24698  reconn  24877  metnrmlem3  24910  cphsubrglem  25227  minveclem1  25474  minveclem3b  25478  ovolficcss  25519  ovolicc2lem4  25570  iundisj2  25599  uniioombllem4  25636  vitalilem5  25662  mbfeqalem1  25691  itg1addlem4  25749  limciun  25944  dvlip2  26045  dv11cn  26051  aalioulem3  26386  pserdvlem2  26479  pserdv  26480  abelthlem2  26483  efif1o  26599  efrlim  27022  lgamgulmlem1  27081  fsumdvdsmul  27247  perfectlem2  27282  noextendseq  27719  nosupno  27755  nosupbnd2lem1  27767  noinfno  27770  noetasuplem4  27788  cuteq1  27898  bdayiun  27996  addbday  28099  oncutlt  28345  oniso  28352  addonbday  28360  bdayn0p1  28450  bdaypw2n0bndlem  28544  setsvtx  29193  uhgredgn0  29286  upgredgss  29290  umgredgss  29291  usgredgss  29317  umgrres1lem  29468  upgrres1  29471  1hegrvtxdg1r  29666  clwlknf1oclwwlknlem3  30242  minvecolem1  31034  sh0le  31600  mdslmd3i  32492  iundisj2f  32750  suppss2f  32801  2ndresdju  32812  fnpreimac  32833  fdifsuppconst  32852  suppss3  32886  iundisj2fi  32960  elrgspnsubrunlem1  33389  erlval  33400  lsmsnorb  33538  extvfvvcl  33793  extvfvcl  33794  esplyind  33833  esplyindfv  33834  esplyfvn  33835  constrextdg2lem  34006  pstmfval  34154  ordtrest2NEW  34181  ldgenpisyslem1  34421  ldgenpisyslem2  34422  omsmeas  34581  sitgclbn  34601  eulerpartlemt  34629  eulerpartlemmf  34633  eulerpartlemgf  34637  bnj849  35181  bnj1136  35253  bnj1311  35280  bnj1413  35291  bnj1452  35308  vonf1oonfo  35419  blsconn  35555  cvmliftlem2  35597  cvmlift2lem12  35625  mvtss  35864  mthmpps  35893  ellcsrspsn  35952  neibastop2lem  36681  filnetlem3  36701  ttcmin  36817  finxpsuclem  37852  poimirlem3  38083  mblfinlem3  38119  areacirclem2  38169  sdclem1  38203  istotbnd3  38231  sstotbnd  38235  iccbnd  38300  icccmpALT  38301  osumcllem1N  40541  osumcllem2N  40542  osumcllem4N  40544  osumcllem9N  40549  pexmidlem6N  40560  dihglblem3N  41880  dvhdimlem  42029  dochexmidlem6  42050  lcfrlem16  42143  lcfr  42170  aks6d1c6lem3  42750  rhmqusspan  42763  ssabdv  42800  hbtlem6  43667  iocinico  43750  oege2  43845  omabs2  43870  tfsconcatb0  43882  trclubgNEW  44155  cnvrcl0  44162  relexp0a  44253  brtrclfv2  44264  cotrclrcl  44279  frege77d  44283  unhe1  44322  ntrrn  44659  imo72b2lem2  44704  imo72b2  44709  mnuprdlem4  44812  radcnvrat  44851  iunconnlem2  45471  ssinss2d  45601  limccog  46157  limsupresico  46235  liminfresico  46306  icccncfext  46422  stoweidlem14  46549  fourierdlem20  46662  fourierdlem42  46684  fourierdlem46  46687  fourierdlem50  46691  fourierdlem51  46692  fourierdlem54  46695  fourierdlem64  46705  fourierdlem76  46717  fourierdlem102  46743  fourierdlem103  46744  fourierdlem104  46745  fourierdlem114  46755  meadjiunlem  47000  meaiininclem  47021  ovnsupge0  47092  hoidmvlelem2  47131  hoidmvlelem4  47133  vonvolmbllem  47195  vonvolmbl2  47198  vonvol2  47199  vonioolem1  47215  preimageiingt  47255  issmflem  47262  fsupdm  47377  finfdm  47381  fundcmpsurinjimaid  47978  perfectALTVlem2  48305  isubgruhgr  48451  uspgropssxp  48727  rhmsubcALTVlem4  48867  srhmsubcALTV  48908  imasubc  49733  imassc  49735  setrec2fun  50274  onsetreclem2  50288