Theorem eqsstrid 3980

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

Syntax hints:   → wi 4   = wceq 1540   ⊆ wss 3898

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2707

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1543  df-ex 1781  df-sb 2067  df-clab 2714  df-cleq 2728  df-clel 2814  df-v 3443  df-in 3905  df-ss 3915

This theorem is referenced by:  eqsstrrid  3981  inss  4185  tpssi  4783  opabssxpd  5665  xpsspw  5751  fun  6687  fmpt  7040  fliftrel  7235  knatar  7284  fr3nr  7684  ordsuci  7721  sucexeloniOLD  7723  suceloniOLD  7725  fiun  7853  f1iun  7854  1stcof  7929  2ndcof  7930  fsplitfpar  8026  fnwelem  8039  oeeui  8504  aceq3lem  9977  cflecard  10110  cfslb2n  10125  itunitc1  10277  axdc3lem2  10308  fpwwe2lem11  10498  canthwelem  10507  wuncval2  10604  peano5nni  12077  un0addcl  12367  un0mulcl  12368  fsuppmapnn0fiublem  13811  fsuppmapnn0fiub  13812  mertenslem2  15696  4sqlem11  16753  4sqlem19  16761  vdwlem13  16791  imasless  17348  rescfth  17750  oppchofcl  18075  oyoncl  18085  mgmidsssn0  18453  cycsubm  18917  efgsfo  19440  efgcpbllemb  19456  frgpuplem  19473  gsummpt1n0  19661  dprdfid  19715  dprd2d2  19742  ablfacrp  19764  ablfac1b  19768  ablfac1eu  19771  pgpfac1lem5  19777  ablfaclem3  19785  lsptpcl  20347  lsppratlem3  20517  lsppratlem4  20518  lbsextlem2  20527  f1lindf  21135  topsn  22186  ordtbaslem  22445  ordtuni  22447  ordtbas2  22448  cnpco  22524  cnconst2  22540  tgcmp  22658  iunconn  22685  ptuni2  22833  xkococnlem  22916  tgqtop  22969  fbasrn  23141  uzrest  23154  fmco  23218  alexsubALT  23308  cnextf  23323  snclseqg  23373  ustund  23479  imasdsf1olem  23632  xmetresbl  23696  blsscls2  23766  metustss  23813  tngtopn  23920  reconn  24097  metnrmlem3  24130  cphsubrglem  24447  minveclem1  24694  minveclem3b  24698  ovolficcss  24739  ovolicc2lem4  24790  iundisj2  24819  uniioombllem4  24856  vitalilem5  24882  mbfeqalem1  24911  itg1addlem4  24969  itg1addlem4OLD  24970  limciun  25164  dvlip2  25265  dv11cn  25271  aalioulem3  25600  pserdvlem2  25693  pserdv  25694  abelthlem2  25697  efif1o  25808  efrlim  26225  lgamgulmlem1  26284  fsumdvdsmul  26450  perfectlem2  26484  noextendseq  26921  nosupno  26957  nosupbnd2lem1  26969  noinfno  26972  noetasuplem4  26990  setsvtx  27694  uhgredgn0  27787  upgredgss  27791  umgredgss  27792  usgredgss  27818  umgrres1lem  27966  upgrres1  27969  1hegrvtxdg1r  28164  clwlknf1oclwwlknlem3  28735  minvecolem1  29524  sh0le  30090  mdslmd3i  30982  iundisj2f  31216  suppss2f  31261  2ndresdju  31273  fnpreimac  31295  fdifsuppconst  31310  suppss3  31346  iundisj2fi  31405  lsmsnorb  31876  pstmfval  32144  ordtrest2NEW  32171  ldgenpisyslem1  32429  ldgenpisyslem2  32430  omsmeas  32590  sitgclbn  32610  eulerpartlemt  32638  eulerpartlemmf  32642  eulerpartlemgf  32646  bnj849  33204  bnj1136  33276  bnj1311  33303  bnj1413  33314  bnj1452  33331  blsconn  33505  cvmliftlem2  33547  cvmlift2lem12  33575  mvtss  33814  mthmpps  33843  neibastop2lem  34645  filnetlem3  34665  finxpsuclem  35681  poimirlem3  35893  mblfinlem3  35929  areacirclem2  35979  sdclem1  36014  istotbnd3  36042  sstotbnd  36046  iccbnd  36111  icccmpALT  36112  osumcllem1N  38232  osumcllem2N  38233  osumcllem4N  38235  osumcllem9N  38240  pexmidlem6N  38251  dihglblem3N  39571  dvhdimlem  39720  dochexmidlem6  39741  lcfrlem16  39834  lcfr  39861  ssabdv  40454  hbtlem6  41225  iocinico  41315  omabs2  41326  trclubgNEW  41556  cnvrcl0  41563  relexp0a  41654  brtrclfv2  41665  cotrclrcl  41680  frege77d  41684  unhe1  41723  ntrrn  42062  imo72b2lem0  42106  imo72b2lem2  42108  imo72b2  42113  mnuprdlem4  42223  radcnvrat  42262  iunconnlem2  42885  ssinss2d  42937  limccog  43506  limsupresico  43586  liminfresico  43657  icccncfext  43773  stoweidlem14  43900  fourierdlem20  44013  fourierdlem42  44035  fourierdlem46  44038  fourierdlem50  44042  fourierdlem51  44043  fourierdlem54  44046  fourierdlem64  44056  fourierdlem76  44068  fourierdlem102  44094  fourierdlem103  44095  fourierdlem104  44096  fourierdlem114  44106  meadjiunlem  44349  meaiininclem  44370  ovnsupge0  44441  hoidmvlelem2  44480  hoidmvlelem4  44482  vonvolmbllem  44544  vonvolmbl2  44547  vonvol2  44548  vonioolem1  44564  issmflem  44611  fundcmpsurinjimaid  45223  perfectALTVlem2  45534  uspgropssxp  45666  funcrngcsetc  45916  funcringcsetc  45953  srhmsubc  45994  rhmsubclem3  46006  srhmsubcALTV  46012  rhmsubcALTVlem4  46025  setrec2fun  46758  onsetreclem2  46771