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

Theorem syl5eqss 3634
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 3614 . 2 (𝐴𝐶𝐵𝐶)
41, 3sylibr 224 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1480  wss 3560
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-in 3567  df-ss 3574
This theorem is referenced by:  syl5eqssr  3635  inss  3826  tpssi  4344  xpsspw  5204  opabssxpd  5308  fun  6033  fmpt  6347  fliftrel  6523  knatar  6572  fr3nr  6941  suceloni  6975  fun11iun  7088  1stcof  7156  2ndcof  7157  fnwelem  7252  oeeui  7642  aceq3lem  8903  cflecard  9035  cfslb2n  9050  itunitc1  9202  axdc3lem2  9233  fpwwe2lem12  9423  canthwelem  9432  wuncval2  9529  peano5nni  10983  un0addcl  11286  un0mulcl  11287  fsuppmapnn0fiublem  12745  fsuppmapnn0fiub  12746  fsuppmapnn0fiubOLD  12747  mertenslem2  14561  4sqlem11  15602  4sqlem19  15610  vdwlem13  15640  imasless  16140  rescfth  16537  oppchofcl  16840  oyoncl  16850  mgmidsssn0  17209  efgsfo  18092  efgcpbllemb  18108  frgpuplem  18125  gsummpt1n0  18304  dprdfid  18356  dprd2d2  18383  ablfacrp  18405  ablfac1b  18409  ablfac1eu  18412  pgpfac1lem5  18418  ablfaclem3  18426  lsptpcl  18919  lsppratlem3  19089  lsppratlem4  19090  lbsextlem2  19099  f1lindf  20101  topsn  20675  ordtbaslem  20932  ordtuni  20934  ordtbas2  20935  cnpco  21011  cnconst2  21027  tgcmp  21144  iunconn  21171  ptuni2  21319  xkococnlem  21402  tgqtop  21455  fbasrn  21628  uzrest  21641  fmco  21705  alexsubALT  21795  cnextf  21810  snclseqg  21859  ustund  21965  imasdsf1olem  22118  xmetresbl  22182  blsscls2  22249  metustss  22296  tngtopn  22394  reconn  22571  metnrmlem3  22604  cphsubrglem  22917  minveclem1  23135  minveclem3b  23139  ovolficcss  23178  ovolicc2lem4  23228  iundisj2  23257  uniioombllem4  23294  vitalilem5  23321  mbfeqalem  23349  itg1addlem4  23406  limciun  23598  dvlip2  23696  dv11cn  23702  aalioulem3  24027  pserdvlem2  24120  pserdv  24121  abelthlem2  24124  efif1o  24230  efrlim  24630  lgamgulmlem1  24689  fsumdvdsmul  24855  perfectlem2  24889  setsvtx  25861  umgrres1lem  26124  upgrres1  26127  1hegrvtxdg1r  26324  minvecolem1  27618  sh0le  28187  mdslmd3i  29079  iundisj2f  29289  suppss2f  29322  suppss3  29386  iundisj2fi  29439  pstmfval  29763  ordtrest2NEW  29793  ldgenpisyslem1  30049  ldgenpisyslem2  30050  omsmeas  30208  sitgclbn  30228  eulerpartlemt  30256  eulerpartlemmf  30260  eulerpartlemgf  30264  bnj849  30756  bnj1136  30826  bnj1311  30853  bnj1413  30864  bnj1452  30881  blsconn  30987  cvmliftlem2  31029  cvmlift2lem12  31057  mvtss  31211  mthmpps  31240  trpredss  31483  trpredmintr  31485  frrlem5d  31541  nosino  31628  neibastop2lem  32050  filnetlem3  32070  finxpsuclem  32905  poimirlem3  33083  mblfinlem3  33119  areacirclem2  33172  sdclem1  33210  istotbnd3  33241  sstotbnd  33245  iccbnd  33310  icccmpALT  33311  osumcllem1N  34761  osumcllem2N  34762  osumcllem4N  34764  osumcllem9N  34769  pexmidlem6N  34780  dihglblem3N  36103  dvhdimlem  36252  dochexmidlem6  36273  lcfrlem16  36366  lcfr  36393  hbtlem6  37219  iocinico  37317  trclubgNEW  37445  cnvrcl0  37452  relexp0a  37528  brtrclfv2  37539  cotrclrcl  37554  frege77d  37558  unhe1  37600  ntrrn  37941  imo72b2lem0  37986  imo72b2lem2  37988  imo72b2lem1  37992  imo72b2  37996  radcnvrat  38034  iunconnlem2  38693  ssinss2d  38750  limccog  39288  limsupresico  39368  icccncfext  39435  stoweidlem14  39568  fourierdlem20  39681  fourierdlem42  39703  fourierdlem46  39706  fourierdlem50  39710  fourierdlem51  39711  fourierdlem54  39714  fourierdlem64  39724  fourierdlem76  39736  fourierdlem102  39762  fourierdlem103  39763  fourierdlem104  39764  fourierdlem114  39774  meadjiunlem  40019  meaiininclem  40037  ovnsupge0  40108  hoidmvlelem2  40147  hoidmvlelem4  40149  vonvolmbllem  40211  vonvolmbl2  40214  vonvol2  40215  vonioolem1  40231  issmflem  40273  perfectALTVlem2  40956  uspgropssxp  41070  funcrngcsetc  41316  funcringcsetc  41353  srhmsubc  41394  rhmsubclem3  41406  srhmsubcALTV  41412  rhmsubcALTVlem4  41425  setrec2fun  41762  onsetreclem2  41772
  Copyright terms: Public domain W3C validator