Theorem syl5eqss 3612

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

Syntax hints:   → wi 4   = wceq 1475   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-in 3547  df-ss 3554

This theorem is referenced by:  syl5eqssr  3613  inss  3804  tpssi  4309  xpsspw  5156  fun  5979  fmpt  6289  fliftrel  6458  knatar  6507  fr3nr  6871  suceloni  6905  opabex2  6997  fun11iun  7019  1stcof  7087  2ndcof  7088  fnwelem  7179  oeeui  7569  aceq3lem  8826  cflecard  8958  cfslb2n  8973  itunitc1  9125  axdc3lem2  9156  fpwwe2lem12  9342  canthwelem  9351  wuncval2  9448  peano5nni  10900  un0addcl  11203  un0mulcl  11204  fsuppmapnn0fiublem  12651  fsuppmapnn0fiub  12652  fsuppmapnn0fiubOLD  12653  mertenslem2  14456  4sqlem11  15497  4sqlem19  15505  vdwlem13  15535  imasless  16023  rescfth  16420  oppchofcl  16723  oyoncl  16733  mgmidsssn0  17092  efgsfo  17975  efgcpbllemb  17991  frgpuplem  18008  gsummpt1n0  18187  dprdfid  18239  dprd2d2  18266  ablfacrp  18288  ablfac1b  18292  ablfac1eu  18295  pgpfac1lem5  18301  ablfaclem3  18309  lsptpcl  18800  lsppratlem3  18970  lsppratlem4  18971  lbsextlem2  18980  f1lindf  19980  topsn  20550  ordtbaslem  20802  ordtuni  20804  ordtbas2  20805  cnpco  20881  cnconst2  20897  tgcmp  21014  iuncon  21041  ptuni2  21189  xkococnlem  21272  tgqtop  21325  fbasrn  21498  uzrest  21511  fmco  21575  alexsubALT  21665  cnextf  21680  snclseqg  21729  ustund  21835  imasdsf1olem  21988  xmetresbl  22052  blsscls2  22119  metustss  22166  tngtopn  22264  reconn  22439  metnrmlem3  22472  cphsubrglem  22785  minveclem1  23003  minveclem3b  23007  ovolficcss  23045  ovolicc2lem4  23095  iundisj2  23124  uniioombllem4  23160  vitalilem5  23187  mbfeqalem  23215  itg1addlem4  23272  limciun  23464  dvlip2  23562  dv11cn  23568  aalioulem3  23893  pserdvlem2  23986  pserdv  23987  abelthlem2  23990  efif1o  24096  efrlim  24496  lgamgulmlem1  24555  fsumdvdsmul  24721  perfectlem2  24755  usgrares1  25939  eupares  26502  minvecolem1  27114  sh0le  27683  mdslmd3i  28575  iundisj2f  28785  suppss2f  28819  suppss3  28890  iundisj2fi  28943  pstmfval  29267  ordtrest2NEW  29297  ldgenpisyslem1  29553  ldgenpisyslem2  29554  omsmeas  29712  sitgclbn  29732  eulerpartlemt  29760  eulerpartlemmf  29764  eulerpartlemgf  29768  bnj849  30249  bnj1136  30319  bnj1311  30346  bnj1413  30357  bnj1452  30374  blscon  30480  cvmliftlem2  30522  cvmlift2lem12  30550  mvtss  30704  mthmpps  30733  trpredss  30973  trpredmintr  30975  frrlem5d  31031  neibastop2lem  31525  filnetlem3  31545  finxpsuclem  32410  poimirlem3  32582  mblfinlem3  32618  areacirclem2  32671  sdclem1  32709  istotbnd3  32740  sstotbnd  32744  iccbnd  32809  icccmpALT  32810  osumcllem1N  34260  osumcllem2N  34261  osumcllem4N  34263  osumcllem9N  34268  pexmidlem6N  34279  dihglblem3N  35602  dvhdimlem  35751  dochexmidlem6  35772  lcfrlem16  35865  lcfr  35892  hbtlem6  36718  iocinico  36816  trclubgNEW  36944  cnvrcl0  36951  relexp0a  37027  brtrclfv2  37038  cotrclrcl  37053  frege77d  37057  unhe1  37099  ntrrn  37440  imo72b2lem0  37487  imo72b2lem2  37489  imo72b2lem1  37493  imo72b2  37497  radcnvrat  37535  iunconlem2  38193  ssinss2d  38253  limccog  38687  icccncfext  38773  stoweidlem14  38907  fourierdlem20  39020  fourierdlem42  39042  fourierdlem46  39045  fourierdlem50  39049  fourierdlem51  39050  fourierdlem54  39053  fourierdlem64  39063  fourierdlem76  39075  fourierdlem102  39101  fourierdlem103  39102  fourierdlem104  39103  fourierdlem114  39113  meadjiunlem  39358  meaiininclem  39376  ovnsupge0  39447  hoidmvlelem2  39486  hoidmvlelem4  39488  vonvolmbllem  39550  vonvolmbl2  39553  vonvol2  39554  vonioolem1  39571  issmflem  39613  perfectALTVlem2  40165  umgrres1lem  40529  upgrres1  40532  1hegrvtxdg1r  40724  funcrngcsetc  41790  funcringcsetc  41827  srhmsubc  41868  rhmsubclem3  41880  srhmsubcALTV  41887  rhmsubcALTVlem4  41900  setrec2fun  42238  onsetreclem2  42248