Theorem eqsstrid 4057

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

Syntax hints:   → wi 4   = wceq 1537   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1778  df-cleq 2732  df-ss 3993

This theorem is referenced by:  eqsstrrid  4058  inss  4268  tpssi  4863  opabssxpd  5747  xpsspw  5833  fun  6783  fmpt  7144  fssrescdmd  7160  fliftrel  7344  knatar  7393  fr3nr  7807  ordsuci  7844  sucexeloniOLD  7846  suceloniOLD  7848  fiun  7983  f1iun  7984  1stcof  8060  2ndcof  8061  fsplitfpar  8159  fnwelem  8172  oeeui  8658  cofon1  8728  aceq3lem  10189  cflecard  10322  cfslb2n  10337  itunitc1  10489  axdc3lem2  10520  fpwwe2lem11  10710  canthwelem  10719  wuncval2  10816  peano5nni  12296  un0addcl  12586  un0mulcl  12587  fsuppmapnn0fiublem  14041  fsuppmapnn0fiub  14042  mertenslem2  15933  4sqlem11  17002  4sqlem19  17010  vdwlem13  17040  imasless  17600  rescfth  18004  oppchofcl  18330  oyoncl  18340  mgmidsssn0  18710  eqg0subg  19236  cycsubm  19242  efgsfo  19781  efgcpbllemb  19797  frgpuplem  19814  gsummpt1n0  20007  dprdfid  20061  dprd2d2  20088  ablfacrp  20110  ablfac1b  20114  ablfac1eu  20117  pgpfac1lem5  20123  ablfaclem3  20131  funcrngcsetc  20662  funcringcsetc  20696  srhmsubc  20702  rhmsubclem3  20709  lsptpcl  21000  lsppratlem3  21174  lsppratlem4  21175  lbsextlem2  21184  f1lindf  21865  topsn  22958  ordtbaslem  23217  ordtuni  23219  ordtbas2  23220  cnpco  23296  cnconst2  23312  tgcmp  23430  iunconn  23457  ptuni2  23605  xkococnlem  23688  tgqtop  23741  fbasrn  23913  uzrest  23926  fmco  23990  alexsubALT  24080  cnextf  24095  snclseqg  24145  ustund  24251  imasdsf1olem  24404  xmetresbl  24468  blsscls2  24538  metustss  24585  tngtopn  24692  reconn  24869  metnrmlem3  24902  cphsubrglem  25230  minveclem1  25477  minveclem3b  25481  ovolficcss  25523  ovolicc2lem4  25574  iundisj2  25603  uniioombllem4  25640  vitalilem5  25666  mbfeqalem1  25695  itg1addlem4  25753  itg1addlem4OLD  25754  limciun  25949  dvlip2  26054  dv11cn  26060  aalioulem3  26394  pserdvlem2  26490  pserdv  26491  abelthlem2  26494  efif1o  26606  efrlim  27030  efrlimOLD  27031  lgamgulmlem1  27090  fsumdvdsmul  27256  fsumdvdsmulOLD  27258  perfectlem2  27292  noextendseq  27730  nosupno  27766  nosupbnd2lem1  27778  noinfno  27781  noetasuplem4  27799  cuteq1  27896  addsbday  28068  setsvtx  29070  uhgredgn0  29163  upgredgss  29167  umgredgss  29168  usgredgss  29194  umgrres1lem  29345  upgrres1  29348  1hegrvtxdg1r  29544  clwlknf1oclwwlknlem3  30115  minvecolem1  30906  sh0le  31472  mdslmd3i  32364  iundisj2f  32612  suppss2f  32657  2ndresdju  32667  fnpreimac  32689  fdifsuppconst  32701  suppss3  32738  iundisj2fi  32802  erlval  33230  lsmsnorb  33384  pstmfval  33842  ordtrest2NEW  33869  ldgenpisyslem1  34127  ldgenpisyslem2  34128  omsmeas  34288  sitgclbn  34308  eulerpartlemt  34336  eulerpartlemmf  34340  eulerpartlemgf  34344  bnj849  34901  bnj1136  34973  bnj1311  35000  bnj1413  35011  bnj1452  35028  blsconn  35212  cvmliftlem2  35254  cvmlift2lem12  35282  mvtss  35521  mthmpps  35550  ellcsrspsn  35609  neibastop2lem  36326  filnetlem3  36346  finxpsuclem  37363  poimirlem3  37583  mblfinlem3  37619  areacirclem2  37669  sdclem1  37703  istotbnd3  37731  sstotbnd  37735  iccbnd  37800  icccmpALT  37801  osumcllem1N  39913  osumcllem2N  39914  osumcllem4N  39916  osumcllem9N  39921  pexmidlem6N  39932  dihglblem3N  41252  dvhdimlem  41401  dochexmidlem6  41422  lcfrlem16  41515  lcfr  41542  aks6d1c6lem3  42129  rhmqusspan  42142  ssabdv  42213  hbtlem6  43086  iocinico  43173  oege2  43269  omabs2  43294  tfsconcatb0  43306  trclubgNEW  43580  cnvrcl0  43587  relexp0a  43678  brtrclfv2  43689  cotrclrcl  43704  frege77d  43708  unhe1  43747  ntrrn  44084  imo72b2lem0  44127  imo72b2lem2  44129  imo72b2  44134  mnuprdlem4  44244  radcnvrat  44283  iunconnlem2  44906  ssinss2d  44962  limccog  45541  limsupresico  45621  liminfresico  45692  icccncfext  45808  stoweidlem14  45935  fourierdlem20  46048  fourierdlem42  46070  fourierdlem46  46073  fourierdlem50  46077  fourierdlem51  46078  fourierdlem54  46081  fourierdlem64  46091  fourierdlem76  46103  fourierdlem102  46129  fourierdlem103  46130  fourierdlem104  46131  fourierdlem114  46141  meadjiunlem  46386  meaiininclem  46407  ovnsupge0  46478  hoidmvlelem2  46517  hoidmvlelem4  46519  vonvolmbllem  46581  vonvolmbl2  46584  vonvol2  46585  vonioolem1  46601  issmflem  46648  fsupdm  46763  finfdm  46767  fundcmpsurinjimaid  47285  perfectALTVlem2  47596  isubgruhgr  47738  uspgropssxp  47867  rhmsubcALTVlem4  48007  srhmsubcALTV  48048  setrec2fun  48784  onsetreclem2  48798