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

Theorem syl5eqss 3682
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 3662 . 2 (𝐴𝐶𝐵𝐶)
41, 3sylibr 224 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wss 3607
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-in 3614  df-ss 3621
This theorem is referenced by:  syl5eqssr  3683  inss  3875  tpssi  4401  xpsspw  5266  opabssxpd  5370  fun  6104  fmpt  6421  fliftrel  6598  knatar  6647  fr3nr  7021  suceloni  7055  fun11iun  7168  1stcof  7240  2ndcof  7241  fnwelem  7337  oeeui  7727  aceq3lem  8981  cflecard  9113  cfslb2n  9128  itunitc1  9280  axdc3lem2  9311  fpwwe2lem12  9501  canthwelem  9510  wuncval2  9607  peano5nni  11061  un0addcl  11364  un0mulcl  11365  fsuppmapnn0fiublem  12829  fsuppmapnn0fiub  12830  fsuppmapnn0fiubOLD  12831  mertenslem2  14661  4sqlem11  15706  4sqlem19  15714  vdwlem13  15744  imasless  16247  rescfth  16644  oppchofcl  16947  oyoncl  16957  mgmidsssn0  17316  efgsfo  18198  efgcpbllemb  18214  frgpuplem  18231  gsummpt1n0  18410  dprdfid  18462  dprd2d2  18489  ablfacrp  18511  ablfac1b  18515  ablfac1eu  18518  pgpfac1lem5  18524  ablfaclem3  18532  lsptpcl  19027  lsppratlem3  19197  lsppratlem4  19198  lbsextlem2  19207  f1lindf  20209  topsn  20783  ordtbaslem  21040  ordtuni  21042  ordtbas2  21043  cnpco  21119  cnconst2  21135  tgcmp  21252  iunconn  21279  ptuni2  21427  xkococnlem  21510  tgqtop  21563  fbasrn  21735  uzrest  21748  fmco  21812  alexsubALT  21902  cnextf  21917  snclseqg  21966  ustund  22072  imasdsf1olem  22225  xmetresbl  22289  blsscls2  22356  metustss  22403  tngtopn  22501  reconn  22678  metnrmlem3  22711  cphsubrglem  23023  minveclem1  23241  minveclem3b  23245  ovolficcss  23284  ovolicc2lem4  23334  iundisj2  23363  uniioombllem4  23400  vitalilem5  23426  mbfeqalem  23454  itg1addlem4  23511  limciun  23703  dvlip2  23803  dv11cn  23809  aalioulem3  24134  pserdvlem2  24227  pserdv  24228  abelthlem2  24231  efif1o  24337  efrlim  24741  lgamgulmlem1  24800  fsumdvdsmul  24966  perfectlem2  25000  setsvtx  25972  uhgredgn0  26068  upgredgss  26072  umgredgss  26073  usgredgss  26099  umgrres1lem  26247  upgrres1  26250  1hegrvtxdg1r  26460  minvecolem1  27858  sh0le  28427  mdslmd3i  29319  iundisj2f  29529  suppss2f  29567  suppss3  29630  iundisj2fi  29684  pstmfval  30067  ordtrest2NEW  30097  ldgenpisyslem1  30354  ldgenpisyslem2  30355  omsmeas  30513  sitgclbn  30533  eulerpartlemt  30561  eulerpartlemmf  30565  eulerpartlemgf  30569  bnj849  31121  bnj1136  31191  bnj1311  31218  bnj1413  31229  bnj1452  31246  blsconn  31352  cvmliftlem2  31394  cvmlift2lem12  31422  mvtss  31576  mthmpps  31605  trpredss  31853  trpredmintr  31855  frrlem5d  31912  noextendseq  31945  nosupno  31974  nosupbnd2lem1  31986  noetalem3  31990  neibastop2lem  32480  filnetlem3  32500  finxpsuclem  33364  poimirlem3  33542  mblfinlem3  33578  areacirclem2  33631  sdclem1  33669  istotbnd3  33700  sstotbnd  33704  iccbnd  33769  icccmpALT  33770  osumcllem1N  35560  osumcllem2N  35561  osumcllem4N  35563  osumcllem9N  35568  pexmidlem6N  35579  dihglblem3N  36901  dvhdimlem  37050  dochexmidlem6  37071  lcfrlem16  37164  lcfr  37191  hbtlem6  38016  iocinico  38114  trclubgNEW  38242  cnvrcl0  38249  relexp0a  38325  brtrclfv2  38336  cotrclrcl  38351  frege77d  38355  unhe1  38396  ntrrn  38737  imo72b2lem0  38782  imo72b2lem2  38784  imo72b2lem1  38788  imo72b2  38792  radcnvrat  38830  iunconnlem2  39485  ssinss2d  39542  limccog  40170  limsupresico  40250  liminfresico  40321  icccncfext  40418  stoweidlem14  40549  fourierdlem20  40662  fourierdlem42  40684  fourierdlem46  40687  fourierdlem50  40691  fourierdlem51  40692  fourierdlem54  40695  fourierdlem64  40705  fourierdlem76  40717  fourierdlem102  40743  fourierdlem103  40744  fourierdlem104  40745  fourierdlem114  40755  meadjiunlem  41000  meaiininclem  41021  ovnsupge0  41092  hoidmvlelem2  41131  hoidmvlelem4  41133  vonvolmbllem  41195  vonvolmbl2  41198  vonvol2  41199  vonioolem1  41215  issmflem  41257  perfectALTVlem2  41956  uspgropssxp  42077  funcrngcsetc  42323  funcringcsetc  42360  srhmsubc  42401  rhmsubclem3  42413  srhmsubcALTV  42419  rhmsubcALTVlem4  42432  setrec2fun  42764  onsetreclem2  42777
  Copyright terms: Public domain W3C validator