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

Theorem syl6reqr 2486
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 2439 . 2  |-  B  =  C
41, 3syl6req 2484 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652
This theorem is referenced by:  iftrue  3737  iffalse  3738  difprsn1  3927  dmmptg  5359  relcoi1  5390  funimacnv  5517  resasplit  5605  dffv3  5716  dfimafn  5767  fniinfv  5777  dffv2  5788  fvco2  5790  zfrep6  5960  fniunfv  5986  isoini  6050  oprabco  6423  riotav  6546  oeeulem  6836  ixpconstg  7063  sbthlem4  7212  sbthlem5  7213  sbthlem6  7214  supval2  7452  hartogslem1  7503  cantnflem1d  7636  alephsuc2  7953  dfac3  7994  xp2cda  8052  hsmexlem5  8302  axdc2lem  8320  gruima  8669  eqneg  9726  zeo  10347  fseq1p1m1  11114  hashfzo  11686  wrdval  11722  s1co  11794  swrds2  11872  fsumtscopo  12573  mulgcd  13038  algcvg  13059  phiprmpw  13157  strfv3  13494  resslem  13514  pwssnf1o  13712  imassca  13737  xpsfrn2  13787  homfeq  13912  oppcbas  13936  resscatc  14252  lubsn  14515  ipotset  14575  ipole  14576  plusfeq  14696  pws0g  14723  frmd0  14797  symgtset  15094  oppgplusfval  15136  sylow3lem2  15254  oppglsm  15268  frgpuplem  15396  frgpupf  15397  frgpup1  15399  frgpup3lem  15401  gsumval3a  15504  gsumzoppg  15531  ablfac1eu  15623  pwsmgp  15716  opprmulfval  15722  dfrhm2  15813  subrg1  15870  staffn  15929  issrngd  15941  scafeq  15962  lbsextlem4  16225  sralem  16241  sravsca  16246  rnascl  16393  psrlinv  16453  opsrbaslem  16530  ply1scl0  16673  zlmlem  16790  zlmvsca  16795  znbaslem  16811  ipfeq  16873  thlbas  16915  thlle  16916  thloc  16918  paste  17350  ptpjcn  17635  uptx  17649  xpstopnlem1  17833  alexsubALTlem4  18073  cnextf  18089  submtmd  18126  ussval  18281  tuslem  18289  psmetge0  18335  xmetge0  18366  setsmsds  18498  tnglem  18673  tngtset  18682  tngngp2  18685  resubmet  18825  pcorev2  19045  om1plusg  19051  om1tset  19052  om1opn  19053  pi1grplem  19066  clmadd  19091  clmmul  19092  clmcj  19093  tchtopn  19176  tchnmfval  19178  bcthlem1  19269  bcthlem2  19270  bcthlem4  19272  bcth3  19276  minveclem3b  19321  pjthlem1  19330  volun  19431  voliun  19440  uniioovol  19463  itg2i1fseq  19639  itgcnlem  19673  iblabslem  19711  limcres  19765  cnplimc  19766  evlseu  19929  evl1sca  19942  mpfsubrg  19953  ply1termlem  20114  0dgr  20156  taylthlem1  20281  abelth  20349  lawcos  20650  basellem8  20862  musum  20968  chtub  20988  dchrval  21010  dchrinvcl  21029  lgsval4lem  21083  lgsquadlem2  21131  m1lgs  21138  2pthlem2  21588  rngoi  21960  drngoi  21987  smcnlem  22185  siii  22346  pjhthlem1  22885  imadifxp  24030  dfimafnf  24035  funcnvmptOLD  24074  funcnvmpt  24075  rdivmuldivd  24219  pstmval  24282  xpinpreima2  24297  pnfneige0  24328  zlmds  24340  zlmtset  24341  esumid  24432  sxsigon  24538  lgambdd  24813  setlikespec  25454  axlowdimlem16  25888  itg2addnclem  26246  iblabsnclem  26258  areacirc  26288  filnetlem4  26401  fnopabco  26415  heiborlem8  26518  mzpcompact2lem  26799  eldioph2lem1  26809  fiphp3d  26871  rmxypairf1o  26965  wopprc  27092  lmhmlnmsplit  27153  dsmmbase  27169  dsmmelbas  27173  frlmelbas  27192  islindf4  27276  psgnunilem2  27386  matbas  27436  matplusg  27437  matsca  27438  matvsca  27439  phisum  27486  dfaimafn  27996  hashimarn  28141  ldualvsub  29890  dalemrotyz  30392  dalem6  30402  dalem7  30403  dalem11  30408  dalem12  30409  dalemrotps  30425  dalem30  30436  dalem35  30441  cdleme1  30961  cdleme9  30987  cdleme20c  31045  cdleme20d  31046  cdlemefrs29clN  31133  cdleme37m  31196  cdleme43aN  31223  cdlemg1b2  31305  cdlemg4f  31349  cdlemh2  31550  erngdvlem1  31722  erngdvlem2N  31723  erngdvlem3  31724  erngdvlem4  31725  erngdvlem1-rN  31730  erngdvlem2-rN  31731  erngdvlem3-rN  31732  erngdvlem4-rN  31733  dvh4dimN  32182  lcdvsub  32352  hlhilsca  32673  hlhilbase  32674  hlhilplus  32675  hlhilvsca  32685  hlhilip  32686  hlhilipval  32687
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator