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

Theorem syl6reqr 2439
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl6reqr.1  |-  ( ph  ->  A  =  B )
syl6reqr.2  |-  C  =  B
Assertion
Ref Expression
syl6reqr  |-  ( ph  ->  C  =  A )

Proof of Theorem syl6reqr
StepHypRef Expression
1 syl6reqr.1 . 2  |-  ( ph  ->  A  =  B )
2 syl6reqr.2 . . 3  |-  C  =  B
32eqcomi 2392 . 2  |-  B  =  C
41, 3syl6req 2437 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  iftrue  3689  iffalse  3690  difprsn1  3879  dmmptg  5308  relcoi1  5339  funimacnv  5466  resasplit  5554  dffv3  5665  dfimafn  5715  fniinfv  5725  dffv2  5736  fvco2  5738  zfrep6  5908  fniunfv  5934  isoini  5998  oprabco  6371  riotav  6491  oeeulem  6781  ixpconstg  7008  sbthlem4  7157  sbthlem5  7158  sbthlem6  7159  supval2  7394  hartogslem1  7445  cantnflem1d  7578  alephsuc2  7895  dfac3  7936  xp2cda  7994  hsmexlem5  8244  axdc2lem  8262  gruima  8611  eqneg  9667  zeo  10288  fseq1p1m1  11053  hashfzo  11622  wrdval  11658  s1co  11730  swrds2  11808  fsumtscopo  12509  mulgcd  12974  algcvg  12995  phiprmpw  13093  strfv3  13430  resslem  13450  pwssnf1o  13648  imassca  13673  xpsfrn2  13723  homfeq  13848  oppcbas  13872  resscatc  14188  lubsn  14451  ipotset  14511  ipole  14512  plusfeq  14632  pws0g  14659  frmd0  14733  symgtset  15030  oppgplusfval  15072  sylow3lem2  15190  oppglsm  15204  frgpuplem  15332  frgpupf  15333  frgpup1  15335  frgpup3lem  15337  gsumval3a  15440  gsumzoppg  15467  ablfac1eu  15559  pwsmgp  15652  opprmulfval  15658  dfrhm2  15749  subrg1  15806  staffn  15865  issrngd  15877  scafeq  15898  lbsextlem4  16161  sralem  16177  sravsca  16182  rnascl  16329  psrlinv  16389  opsrbaslem  16466  ply1scl0  16609  zlmlem  16722  zlmvsca  16727  znbaslem  16743  ipfeq  16805  thlbas  16847  thlle  16848  thloc  16850  paste  17281  ptpjcn  17565  uptx  17579  xpstopnlem1  17763  alexsubALTlem4  18003  cnextf  18019  submtmd  18056  ussval  18211  tuslem  18219  xmetge0  18284  setsmsds  18397  tnglem  18553  tngtset  18562  tngngp2  18565  resubmet  18705  pcorev2  18925  om1plusg  18931  om1tset  18932  om1opn  18933  pi1grplem  18946  clmadd  18971  clmmul  18972  clmcj  18973  tchtopn  19056  tchnmfval  19058  bcthlem1  19147  bcthlem2  19148  bcthlem4  19150  bcth3  19154  minveclem3b  19197  pjthlem1  19206  volun  19307  voliun  19316  uniioovol  19339  itg2i1fseq  19515  itgcnlem  19549  iblabslem  19587  limcres  19641  cnplimc  19642  evlseu  19805  evl1sca  19818  mpfsubrg  19829  ply1termlem  19990  0dgr  20032  taylthlem1  20157  abelth  20225  lawcos  20526  basellem8  20738  musum  20844  chtub  20864  dchrval  20886  dchrinvcl  20905  lgsval4lem  20959  lgsquadlem2  21007  m1lgs  21014  2pthonlem2  21449  rngoi  21817  drngoi  21844  smcnlem  22042  siii  22203  pjhthlem1  22742  imadifxp  23882  dfimafnf  23887  funcnvmptOLD  23924  funcnvmpt  23925  rdivmuldivd  24057  xpinpreima2  24110  pnfneige0  24141  zlmds  24150  zlmtset  24151  esumid  24237  sxsigon  24343  lgambdd  24601  setlikespec  25212  axlowdimlem16  25611  iblabsnclem  25969  areacirc  25989  filnetlem4  26102  fnopabco  26116  heiborlem8  26219  mzpcompact2lem  26500  eldioph2lem1  26510  fiphp3d  26572  rmxypairf1o  26666  wopprc  26793  lmhmlnmsplit  26855  dsmmbase  26871  dsmmelbas  26875  frlmelbas  26894  islindf4  26978  psgnunilem2  27088  matbas  27138  matplusg  27139  matsca  27140  matvsca  27141  phisum  27188  dfaimafn  27699  ldualvsub  29271  dalemrotyz  29773  dalem6  29783  dalem7  29784  dalem11  29789  dalem12  29790  dalemrotps  29806  dalem30  29817  dalem35  29822  cdleme1  30342  cdleme9  30368  cdleme20c  30426  cdleme20d  30427  cdlemefrs29clN  30514  cdleme37m  30577  cdleme43aN  30604  cdlemg1b2  30686  cdlemg4f  30730  cdlemh2  30931  erngdvlem1  31103  erngdvlem2N  31104  erngdvlem3  31105  erngdvlem4  31106  erngdvlem1-rN  31111  erngdvlem2-rN  31112  erngdvlem3-rN  31113  erngdvlem4-rN  31114  dvh4dimN  31563  lcdvsub  31733  hlhilsca  32054  hlhilbase  32055  hlhilplus  32056  hlhilvsca  32066  hlhilip  32067  hlhilipval  32068
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-11 1753  ax-ext 2369
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2381
  Copyright terms: Public domain W3C validator