Theorem syl5eqss 3874

Description: A chained subclass and equality deduction. (Contributed by NM, 25-Apr-2004.)

Hypotheses

Ref	Expression
syl5eqss.1	⊢ 𝐴 = 𝐵
syl5eqss.2	⊢ (𝜑 → 𝐵 ⊆ 𝐶)

Assertion

Ref	Expression
syl5eqss	⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Proof of Theorem syl5eqss

Step	Hyp	Ref	Expression
1		syl5eqss.2	. 2 ⊢ (𝜑 → 𝐵 ⊆ 𝐶)
2		syl5eqss.1	. . 3 ⊢ 𝐴 = 𝐵
3	2	sseq1i 3854	. 2 ⊢ (𝐴 ⊆ 𝐶 ↔ 𝐵 ⊆ 𝐶)
4	1, 3	sylibr 226	1 ⊢ (𝜑 → 𝐴 ⊆ 𝐶)

Syntax hints:   → wi 4   = wceq 1656   ⊆ wss 3798

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1894  ax-4 1908  ax-5 2009  ax-6 2075  ax-7 2112  ax-9 2173  ax-10 2192  ax-11 2207  ax-12 2220  ax-ext 2803

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 879  df-tru 1660  df-ex 1879  df-nf 1883  df-sb 2068  df-clab 2812  df-cleq 2818  df-clel 2821  df-in 3805  df-ss 3812

This theorem is referenced by:  syl5eqssr  3875  inss  4069  tpssi  4587  xpsspw  5471  opabssxpd  5574  fun  6307  fmpt  6634  fliftrel  6818  knatar  6867  fr3nr  7245  suceloni  7279  fun11iun  7393  1stcof  7463  2ndcof  7464  fnwelem  7561  oeeui  7954  aceq3lem  9263  cflecard  9397  cfslb2n  9412  itunitc1  9564  axdc3lem2  9595  fpwwe2lem12  9785  canthwelem  9794  wuncval2  9891  peano5nni  11360  un0addcl  11660  un0mulcl  11661  fsuppmapnn0fiublem  13091  fsuppmapnn0fiub  13092  mertenslem2  14997  4sqlem11  16037  4sqlem19  16045  vdwlem13  16075  imasless  16560  rescfth  16956  oppchofcl  17260  oyoncl  17270  mgmidsssn0  17629  efgsfo  18511  efgcpbllemb  18528  frgpuplem  18545  gsummpt1n0  18724  dprdfid  18777  dprd2d2  18804  ablfacrp  18826  ablfac1b  18830  ablfac1eu  18833  pgpfac1lem5  18839  ablfaclem3  18847  lsptpcl  19345  lsppratlem3  19517  lsppratlem4  19518  lbsextlem2  19527  f1lindf  20535  topsn  21113  ordtbaslem  21370  ordtuni  21372  ordtbas2  21373  cnpco  21449  cnconst2  21465  tgcmp  21582  iunconn  21609  ptuni2  21757  xkococnlem  21840  tgqtop  21893  fbasrn  22065  uzrest  22078  fmco  22142  alexsubALT  22232  cnextf  22247  snclseqg  22296  ustund  22402  imasdsf1olem  22555  xmetresbl  22619  blsscls2  22686  metustss  22733  tngtopn  22831  reconn  23008  metnrmlem3  23041  cphsubrglem  23353  minveclem1  23599  minveclem3b  23603  ovolficcss  23642  ovolicc2lem4  23693  iundisj2  23722  uniioombllem4  23759  vitalilem5  23785  mbfeqalem1  23814  itg1addlem4  23872  limciun  24064  dvlip2  24164  dv11cn  24170  aalioulem3  24495  pserdvlem2  24588  pserdv  24589  abelthlem2  24592  efif1o  24699  efrlim  25116  lgamgulmlem1  25175  fsumdvdsmul  25341  perfectlem2  25375  setsvtx  26340  uhgredgn0  26433  upgredgss  26437  umgredgss  26438  usgredgss  26465  umgrres1lem  26614  upgrres1  26617  1hegrvtxdg1r  26813  clwlknf1oclwwlknlem3  27450  clwlknf1oclwwlknlem3OLD  27452  minvecolem1  28281  sh0le  28850  mdslmd3i  29742  iundisj2f  29946  suppss2f  29984  suppss3  30046  iundisj2fi  30099  pstmfval  30480  ordtrest2NEW  30510  ldgenpisyslem1  30767  ldgenpisyslem2  30768  omsmeas  30926  sitgclbn  30946  eulerpartlemt  30974  eulerpartlemmf  30978  eulerpartlemgf  30982  bnj849  31537  bnj1136  31607  bnj1311  31634  bnj1413  31645  bnj1452  31662  blsconn  31768  cvmliftlem2  31810  cvmlift2lem12  31838  mvtss  31992  mthmpps  32021  trpredss  32262  trpredmintr  32264  frrlem5d  32321  noextendseq  32354  nosupno  32383  nosupbnd2lem1  32395  noetalem3  32399  neibastop2lem  32888  filnetlem3  32908  finxpsuclem  33774  poimirlem3  33951  mblfinlem3  33987  areacirclem2  34039  sdclem1  34076  istotbnd3  34107  sstotbnd  34111  iccbnd  34176  icccmpALT  34177  osumcllem1N  36026  osumcllem2N  36027  osumcllem4N  36029  osumcllem9N  36034  pexmidlem6N  36045  dihglblem3N  37365  dvhdimlem  37514  dochexmidlem6  37535  lcfrlem16  37628  lcfr  37655  hbtlem6  38537  iocinico  38634  trclubgNEW  38761  cnvrcl0  38768  relexp0a  38844  brtrclfv2  38855  cotrclrcl  38870  frege77d  38874  unhe1  38914  ntrrn  39255  imo72b2lem0  39300  imo72b2lem2  39302  imo72b2lem1  39306  imo72b2  39310  radcnvrat  39348  iunconnlem2  39984  ssinss2d  40040  limccog  40641  limsupresico  40721  liminfresico  40792  icccncfext  40889  stoweidlem14  41019  fourierdlem20  41132  fourierdlem42  41154  fourierdlem46  41157  fourierdlem50  41161  fourierdlem51  41162  fourierdlem54  41165  fourierdlem64  41175  fourierdlem76  41187  fourierdlem102  41213  fourierdlem103  41214  fourierdlem104  41215  fourierdlem114  41225  meadjiunlem  41467  meaiininclem  41488  ovnsupge0  41559  hoidmvlelem2  41598  hoidmvlelem4  41600  vonvolmbllem  41662  vonvolmbl2  41665  vonvol2  41666  vonioolem1  41682  issmflem  41724  perfectALTVlem2  42475  uspgropssxp  42613  funcrngcsetc  42859  funcringcsetc  42896  srhmsubc  42937  rhmsubclem3  42949  srhmsubcALTV  42955  rhmsubcALTVlem4  42968  setrec2fun  43344  onsetreclem2  43357