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

Theorem syl5eleqr 2737
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 2657 . 2 (𝜑𝐵 = 𝐶)
41, 3syl5eleq 2736 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  wcel 2030
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-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644  df-clel 2647
This theorem is referenced by:  rabsnt  4298  onnev  5886  opabiota  6300  canth  6648  onnseq  7486  tfrlem16  7534  oen0  7711  nnawordex  7762  inf0  8556  cantnflt  8607  cnfcom2  8637  cnfcom3lem  8638  cnfcom3  8639  r1ordg  8679  r1val1  8687  rankr1id  8763  acacni  9000  dfacacn  9001  dfac13  9002  cda1dif  9036  ttukeylem5  9373  ttukeylem6  9374  gch2  9535  gch3  9536  gchac  9541  gchina  9559  swrds1  13497  wrdl3s3  13751  sadcp1  15224  lcmfunsnlem2  15400  xpsfrnel2  16272  idfucl  16588  gsumval2  17327  gsumz  17421  frmdmnd  17443  frmd0  17444  efginvrel2  18186  efgcpbl2  18216  pgpfaclem1  18526  lbsexg  19212  zringndrg  19886  frlmlbs  20184  mat0dimscm  20323  mat0scmat  20392  m2detleiblem5  20479  m2detleiblem6  20480  m2detleiblem3  20483  m2detleiblem4  20484  d0mat2pmat  20591  chpmat0d  20687  dfac14  21469  acufl  21768  cnextfvval  21916  cnextcn  21918  minveclem3b  23245  minveclem4a  23247  ovollb2  23303  ovolunlem1a  23310  ovolunlem1  23311  ovoliunlem1  23316  ovoliun2  23320  ioombl1lem4  23375  uniioombllem1  23395  uniioombllem2  23397  uniioombllem6  23402  itg2monolem1  23562  itg2mono  23565  itg2cnlem1  23573  xrlimcnp  24740  efrlim  24741  eengbas  25906  ebtwntg  25907  ecgrtg  25908  elntg  25909  wlkl1loop  26590  elwwlks2ons3im  26919  elwwlks2ons3OLD  26921  upgr3v3e3cycl  27158  upgr4cycl4dv4e  27163  2clwwlk2clwwlklem2lem2  27329  2clwwlk2clwwlk  27338  ex-br  27418  rge0scvg  30123  repr0  30817  hgt750lemg  30860  mrsub0  31539  elmrsubrn  31543  topjoin  32485  pclfinN  35504  aomclem1  37941  dfac21  37953  clsk1indlem1  38660  fourierdlem102  40743  fourierdlem114  40755  lincval0  42529  lcoel0  42542
  Copyright terms: Public domain W3C validator