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

Theorem syl6reqr 2875
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl6reqr.1 (𝜑𝐴 = 𝐵)
syl6reqr.2 𝐶 = 𝐵
Assertion
Ref Expression
syl6reqr (𝜑𝐶 = 𝐴)

Proof of Theorem syl6reqr
StepHypRef Expression
1 syl6reqr.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6reqr.2 . . 3 𝐶 = 𝐵
32eqcomi 2830 . 2 𝐵 = 𝐶
41, 3syl6req 2873 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-9 2125  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-ex 1782  df-cleq 2814
This theorem is referenced by:  iftrue  4446  iffalse  4449  difprsn1  4706  dmmptg  6069  setlikespec  6142  funimacnv  6408  dmmptd  6466  resasplit  6521  dffv3  6639  dfimafn  6701  fniinfv  6715  dffv2  6729  fvco2  6731  fniunfv  6980  isoini  7065  fvmpopr2d  7285  zfrep6  7631  oprabco  7766  suppco  7845  oeeulem  8202  ixpconstg  8445  sbthlem4  8606  sbthlem5  8607  sbthlem6  8608  supval2  8895  hartogslem1  8982  cantnflem1d  9127  alephsuc2  9483  dfac3  9524  hsmexlem5  9829  axdc2lem  9847  gruima  10201  eqneg  11337  zeo  12046  fseq1p1m1  12964  hashfzo  13774  hashimarn  13785  wrdval  13848  wrdnval  13876  repswswrd  14125  s1co  14174  swrds2  14281  modfsummod  15128  telfsumo  15136  mulgcd  15873  algcvg  15897  phiprmpw  16090  phisum  16104  strfv3  16510  resslem  16535  pwssnf1o  16749  imassca  16770  homfeq  16942  oppcbas  16966  resscatc  17343  estrcbasbas  17359  funcestrcsetclem7  17374  funcestrcsetclem8  17375  funcestrcsetclem9  17376  fthestrcsetc  17378  fullestrcsetc  17379  equivestrcsetc  17380  setc1strwun  17381  funcsetcestrclem7  17389  funcsetcestrclem8  17390  funcsetcestrclem9  17391  fthsetcestrc  17393  fullsetcestrc  17394  lubsn  17682  ipotset  17745  ipole  17746  plusfeq  17838  pws0g  17925  frmd0  18003  efmndtset  18022  oppgplusfval  18454  gsmsymgrfix  18534  gsmsymgreq  18538  psgnunilem2  18601  sylow3lem2  18731  oppglsm  18745  frgpuplem  18876  frgpupf  18877  frgpup1  18879  frgpup3lem  18881  gsumzoppg  19042  ablfac1eu  19173  pgpfaclem1  19181  pwsmgp  19346  opprmulfval  19353  dfrhm2  19447  subrg1  19520  staffn  19595  issrngd  19607  scafeq  19629  lbsextlem4  19908  sralem  19924  sravsca  19929  sraip  19930  rnascl  20095  psrlinv  20152  opsrbaslem  20233  evlseu  20271  mpfsubrg  20291  ply1scl0  20433  evl1sca  20472  evls1var  20476  zlmlem  20639  zlmvsca  20644  znbaslem  20660  ipfeq  20769  ssipeq  20775  thlbas  20815  thlle  20816  thloc  20818  dsmmbase  20854  dsmmelbas  20858  frlmelbas  20875  frlmphl  20900  islindf4  20957  matbas  20997  matplusg  20998  matsca  20999  matvsca  21000  matbas2d  21007  matsubgcell  21018  matmulcell  21029  ofco2  21035  mattposm  21043  mat1f1o  21062  mdetunilem8  21203  madugsum  21227  cramerimplem2  21268  decpmatmullem  21354  paste  21877  ptpjcn  22194  uptx  22208  xpstopnlem1  22392  alexsubALTlem4  22633  cnextf  22649  submtmd  22687  ussval  22843  tuslem  22851  psmetge0  22897  xmetge0  22929  setsmsds  23061  sgrim  23215  tnglem  23224  tngtset  23233  tngngp2  23236  resubmet  23385  pcorev2  23611  om1plusg  23617  om1tset  23618  om1opn  23619  pi1grplem  23632  clmadd  23657  clmmul  23658  clmcj  23659  tcphtopn  23808  tchnmfval  23810  bcthlem1  23906  bcthlem2  23907  bcthlem4  23909  bcth3  23913  rrxmval  23987  rrxmfval  23988  rrxdsfi  23993  ehlbase  23997  minveclem3b  24010  pjthlem1  24019  volun  24127  voliun  24136  uniioovol  24161  itg2i1fseq  24337  itgcnlem  24371  iblabslem  24409  limcres  24467  cnplimc  24468  ply1termlem  24778  0dgr  24820  taylthlem1  24946  abelth  25014  lawcos  25380  lgambdd  25600  basellem8  25651  musum  25754  chtub  25774  dchrval  25796  dchrinvcl  25815  lgsval4lem  25870  lgsquadlem2  25943  m1lgs  25950  mirauto  26456  lmiisolem  26568  ttglem  26648  axlowdimlem16  26729  ebtwntg  26754  ecgrtg  26755  elntg2  26757  nbgrval  27104  uvtxupgrres  27176  clwlknf1oclwwlknlem3  27846  eucrct2eupth  28008  smcnlem  28458  siii  28614  pjhthlem1  29152  sbcies  30235  imadifxp  30337  dfimafnf  30367  funcnvmpt  30398  symgcom  30734  cycpmconjslem1  30803  rdivmuldivd  30869  resvlem  30911  qusker  30925  mdetpmtr12  31100  pstmval  31145  xpinpreima2  31157  pnfneige0  31201  zlmds  31212  zlmtset  31213  esumid  31310  esumrnmpt  31318  sxsigon  31458  carsgclctunlem1  31582  circlemethnat  31919  f1resfz0f1d  32368  pthhashvtx  32381  filnetlem4  33736  setsstrset  34444  finxpreclem4  34691  itg2addnclem  34986  iblabsnclem  34998  areacirc  35028  fnopabco  35039  heiborlem8  35134  rngoi  35215  drngoi  35267  ldualvsub  36329  dalemrotyz  36832  dalem6  36842  dalem7  36843  dalem11  36848  dalem12  36849  dalemrotps  36865  dalem30  36876  dalem35  36881  cdleme1  37401  cdleme9  37427  cdleme20c  37485  cdleme20d  37486  cdlemefrs29clN  37573  cdleme37m  37636  cdleme43aN  37663  cdlemg1b2  37745  cdlemg4f  37789  cdlemh2  37990  erngdvlem1  38162  erngdvlem2N  38163  erngdvlem3  38164  erngdvlem4  38165  erngdvlem1-rN  38170  erngdvlem2-rN  38171  erngdvlem3-rN  38172  erngdvlem4-rN  38173  dvh4dimN  38621  lcdvsub  38791  hlhilsca  39109  hlhilbase  39110  hlhilplus  39111  hlhilvsca  39121  hlhilip  39122  hlhilipval  39123  rnasclg  39245  uvcn0  39273  prjspeclsp  39401  mzpcompact2lem  39487  eldioph2lem1  39496  fiphp3d  39555  rmxypairf1o  39647  wopprc  39766  lmhmlnmsplit  39826  clcnvlem  40118  mnringnmulrd  40705  mnringbaserd  40707  mnringmulrd  40714  dmmptdf  41642  dmmptdf2  41657  ellimcabssub0  42050  cosknegpi  42302  fourierdlem58  42597  fourierdlem59  42598  fourierdlem72  42611  fourierdlem80  42619  sqwvfourb  42662  etransclem28  42695  etransclem41  42708  omef  42926  dfaimafn  43512  afv2co2  43604  sbgoldbo  44097  rrxlinesc  44909  rrxlinec  44910  rrx2linest2  44918  rrxsphere  44922  itsclinecirc0b  44948  itsclquadb  44950
  Copyright terms: Public domain W3C validator