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

Theorem syl5eleqr 2694
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 2615 . 2 (𝜑𝐵 = 𝐶)
41, 3syl5eleq 2693 1 (𝜑𝐴𝐶)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  wcel 1976
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-ext 2589
This theorem depends on definitions:  df-bi 195  df-an 384  df-ex 1695  df-cleq 2602  df-clel 2605
This theorem is referenced by:  rabsnt  4209  onnev  5751  opabiota  6156  canth  6486  onnseq  7305  tfrlem16  7353  oen0  7530  nnawordex  7581  inf0  8378  cantnflt  8429  cnfcom2  8459  cnfcom3lem  8460  cnfcom3  8461  r1ordg  8501  r1val1  8509  rankr1id  8585  acacni  8822  dfacacn  8823  dfac13  8824  cda1dif  8858  ttukeylem5  9195  ttukeylem6  9196  gch2  9353  gch3  9354  gchac  9359  gchina  9377  swrds1  13249  wrdl3s3  13499  sadcp1  14961  lcmfunsnlem2  15137  xpsfrnel2  15994  idfucl  16310  gsumval2  17049  gsumz  17143  frmdmnd  17165  frmd0  17166  efginvrel2  17909  efgcpbl2  17939  pgpfaclem1  18249  lbsexg  18931  frlmlbs  19897  mat0dimscm  20036  mat0scmat  20105  m2detleiblem5  20192  m2detleiblem6  20193  m2detleiblem3  20196  m2detleiblem4  20197  d0mat2pmat  20304  chpmat0d  20400  dfac14  21173  acufl  21473  cnextfvval  21621  cnextcn  21623  minveclem3b  22924  minveclem4a  22926  ovollb2  22981  ovolunlem1a  22988  ovolunlem1  22989  ovoliunlem1  22994  ovoliun2  22998  ioombl1lem4  23053  uniioombllem1  23072  uniioombllem2  23074  uniioombllem6  23079  itg2monolem1  23240  itg2mono  23243  itg2cnlem1  23251  xrlimcnp  24412  efrlim  24413  eengbas  25579  ebtwntg  25580  ecgrtg  25581  elntg  25582  cusgrares  25767  usgrcyclnl1  25934  ex-br  26446  vcoprneOLD  26600  rge0scvg  29129  mrsub0  30473  elmrsubrn  30477  topjoin  31336  pclfinN  34000  aomclem1  36438  dfac21  36450  clsk1indlem1  37159  fourierdlem102  38898  fourierdlem114  38910  1wlkl1loop  40837  wwlks2onv  41153  elwwlks2ons3  41154  upgr3v3e3cycl  41342  upgr4cycl4dv4e  41347  lincval0  41993  lcoel0  42006
  Copyright terms: Public domain W3C validator