MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl5eqss Structured version   Visualization version   GIF version

Theorem syl5eqss 3608
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
StepHypRef Expression
1 syl5eqss.2 . 2 (𝜑𝐵𝐶)
2 syl5eqss.1 . . 3 𝐴 = 𝐵
32sseq1i 3588 . 2 (𝐴𝐶𝐵𝐶)
41, 3sylibr 222 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wss 3536
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2229  ax-ext 2586
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2593  df-cleq 2599  df-clel 2602  df-in 3543  df-ss 3550
This theorem is referenced by:  syl5eqssr  3609  inss  3800  tpssi  4301  xpsspw  5142  fun  5962  fmpt  6271  fliftrel  6433  knatar  6482  fr3nr  6845  suceloni  6879  opabex2  6971  fun11iun  6993  1stcof  7061  2ndcof  7062  fnwelem  7153  oeeui  7543  aceq3lem  8800  cflecard  8932  cfslb2n  8947  itunitc1  9099  axdc3lem2  9130  fpwwe2lem12  9316  canthwelem  9325  wuncval2  9422  peano5nni  10867  un0addcl  11170  un0mulcl  11171  fsuppmapnn0fiublem  12603  fsuppmapnn0fiub  12604  fsuppmapnn0fiubOLD  12605  mertenslem2  14399  4sqlem11  15440  4sqlem19  15448  vdwlem13  15478  imasless  15966  rescfth  16363  oppchofcl  16666  oyoncl  16676  mgmidsssn0  17035  efgsfo  17918  efgcpbllemb  17934  frgpuplem  17951  gsummpt1n0  18130  dprdfid  18182  dprd2d2  18209  ablfacrp  18231  ablfac1b  18235  ablfac1eu  18238  pgpfac1lem5  18244  ablfaclem3  18252  lsptpcl  18743  lsppratlem3  18913  lsppratlem4  18914  lbsextlem2  18923  f1lindf  19919  topsn  20489  ordtbaslem  20741  ordtuni  20743  ordtbas2  20744  cnpco  20820  cnconst2  20836  tgcmp  20953  iuncon  20980  ptuni2  21128  xkococnlem  21211  tgqtop  21264  fbasrn  21437  uzrest  21450  fmco  21514  alexsubALT  21604  cnextf  21619  snclseqg  21668  ustund  21774  imasdsf1olem  21926  xmetresbl  21990  blsscls2  22057  metustss  22104  tngtopn  22199  reconn  22368  metnrmlem3  22400  cphsubrglem  22706  minveclem1  22917  minveclem3b  22921  ovolficcss  22959  ovolicc2lem4  23009  iundisj2  23038  uniioombllem4  23074  vitalilem5  23101  mbfeqalem  23129  itg1addlem4  23186  limciun  23378  dvlip2  23476  dv11cn  23482  aalioulem3  23807  pserdvlem2  23900  pserdv  23901  abelthlem2  23904  efif1o  24010  efrlim  24410  lgamgulmlem1  24469  fsumdvdsmul  24635  perfectlem2  24669  usgrares1  25702  eupares  26265  minvecolem1  26917  sh0le  27486  mdslmd3i  28378  iundisj2f  28588  suppss2f  28622  suppss3  28693  iundisj2fi  28746  pstmfval  29070  ordtrest2NEW  29100  ldgenpisyslem1  29356  ldgenpisyslem2  29357  omsmeas  29515  sitgclbn  29535  eulerpartlemt  29563  eulerpartlemmf  29567  eulerpartlemgf  29571  bnj849  30052  bnj1136  30122  bnj1311  30149  bnj1413  30160  bnj1452  30177  blscon  30283  cvmliftlem2  30325  cvmlift2lem12  30353  mvtss  30507  mthmpps  30536  trpredss  30776  trpredmintr  30778  frrlem5d  30834  neibastop2lem  31328  filnetlem3  31348  finxpsuclem  32210  poimirlem3  32382  mblfinlem3  32418  areacirclem2  32471  sdclem1  32509  istotbnd3  32540  sstotbnd  32544  iccbnd  32609  icccmpALT  32610  osumcllem1N  34060  osumcllem2N  34061  osumcllem4N  34063  osumcllem9N  34068  pexmidlem6N  34079  dihglblem3N  35402  dvhdimlem  35551  dochexmidlem6  35572  lcfrlem16  35665  lcfr  35692  hbtlem6  36518  iocinico  36616  trclubgNEW  36744  cnvrcl0  36751  relexp0a  36827  brtrclfv2  36838  cotrclrcl  36853  frege77d  36857  unhe1  36899  ntrrn  37240  imo72b2lem0  37287  imo72b2lem2  37289  imo72b2lem1  37293  imo72b2  37297  radcnvrat  37335  iunconlem2  37993  ssinss2d  38053  limccog  38488  icccncfext  38574  stoweidlem14  38708  fourierdlem20  38821  fourierdlem42  38843  fourierdlem46  38846  fourierdlem50  38850  fourierdlem51  38851  fourierdlem54  38854  fourierdlem64  38864  fourierdlem76  38876  fourierdlem102  38902  fourierdlem103  38903  fourierdlem104  38904  fourierdlem114  38914  meadjiunlem  39159  meaiininclem  39177  ovnsupge0  39248  hoidmvlelem2  39287  hoidmvlelem4  39289  vonvolmbllem  39351  vonvolmbl2  39354  vonvol2  39355  vonioolem1  39372  issmflem  39414  perfectALTVlem2  39967  umgrres1lem  40528  upgrres1  40531  1hegrvtxdg1r  40723  funcrngcsetc  41789  funcringcsetc  41826  srhmsubc  41867  rhmsubclem3  41879  srhmsubcALTV  41886  rhmsubcALTVlem4  41899
  Copyright terms: Public domain W3C validator