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

Theorem syl5eleqr 2847
Description: A membership and equality inference. (Contributed by NM, 4-Jan-2006.)
Hypotheses
Ref Expression
syl5eleqr.1 𝐴𝐵
syl5eleqr.2 (𝜑𝐶 = 𝐵)
Assertion
Ref Expression
syl5eleqr (𝜑𝐴𝐶)

Proof of Theorem syl5eleqr
StepHypRef Expression
1 syl5eleqr.1 . 2 𝐴𝐵
2 syl5eleqr.2 . . 3 (𝜑𝐶 = 𝐵)
32eqcomd 2767 . 2 (𝜑𝐵 = 𝐶)
41, 3syl5eleq 2846 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  wcel 2140
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-ext 2741
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1854  df-cleq 2754  df-clel 2757
This theorem is referenced by:  rabsnt  4411  onnev  6010  opabiota  6425  canth  6773  onnseq  7612  tfrlem16  7660  oen0  7838  nnawordex  7889  inf0  8694  cantnflt  8745  cnfcom2  8775  cnfcom3lem  8776  cnfcom3  8777  r1ordg  8817  r1val1  8825  rankr1id  8901  acacni  9175  dfacacn  9176  dfac13  9177  cda1dif  9211  ttukeylem5  9548  ttukeylem6  9549  gch2  9710  gch3  9711  gchac  9716  gchina  9734  swrds1  13672  wrdl3s3  13927  sadcp1  15400  lcmfunsnlem2  15576  xpsfrnel2  16448  idfucl  16763  gsumval2  17502  gsumz  17596  frmdmnd  17618  frmd0  17619  efginvrel2  18361  efgcpbl2  18391  pgpfaclem1  18701  lbsexg  19387  zringndrg  20061  frlmlbs  20359  mat0dimscm  20498  mat0scmat  20567  m2detleiblem5  20654  m2detleiblem6  20655  m2detleiblem3  20658  m2detleiblem4  20659  d0mat2pmat  20766  chpmat0d  20862  dfac14  21644  acufl  21943  cnextfvval  22091  cnextcn  22093  minveclem3b  23420  minveclem4a  23422  ovollb2  23478  ovolunlem1a  23485  ovolunlem1  23486  ovoliunlem1  23491  ovoliun2  23495  ioombl1lem4  23550  uniioombllem1  23570  uniioombllem2  23572  uniioombllem6  23577  itg2monolem1  23737  itg2mono  23740  itg2cnlem1  23748  xrlimcnp  24916  efrlim  24917  eengbas  26082  ebtwntg  26083  ecgrtg  26084  elntg  26085  wlkl1loop  26766  elwwlks2ons3im  27096  elwwlks2ons3OLD  27098  upgr3v3e3cycl  27354  upgr4cycl4dv4e  27359  2clwwlk2clwwlk  27529  ex-br  27621  rge0scvg  30326  repr0  31020  hgt750lemg  31063  mrsub0  31742  elmrsubrn  31746  topjoin  32688  pclfinN  35708  aomclem1  38145  dfac21  38157  clsk1indlem1  38864  fourierdlem102  40947  fourierdlem114  40959  lincval0  42733  lcoel0  42746
  Copyright terms: Public domain W3C validator