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

Theorem syl6reqr 2334
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 2287 . 2  |-  B  =  C
41, 3syl6req 2332 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  iftrue  3571  iffalse  3572  dmmptg  5170  relcoi1  5201  funimacnv  5324  resasplit  5411  dffv3  5521  dfimafn  5571  fniinfv  5581  dffv2  5592  fvco2  5594  zfrep6  5748  fniunfv  5773  isoini  5835  oprabco  6203  riotav  6309  oeeulem  6599  ixpconstg  6825  sbthlem4  6974  sbthlem5  6975  sbthlem6  6976  supval2  7206  hartogslem1  7257  cantnflem1d  7390  alephsuc2  7707  dfac3  7748  xp2cda  7806  hsmexlem5  8056  axdc2lem  8074  gruima  8424  eqneg  9480  zeo  10097  fseq1p1m1  10857  hashfzo  11383  wrdval  11416  s1co  11488  swrds2  11560  fsumtscopo  12260  mulgcd  12725  algcvg  12746  phiprmpw  12844  strfv3  13181  resslem  13201  pwssnf1o  13397  imassca  13422  xpsfrn2  13472  homfeq  13597  oppcbas  13621  resscatc  13937  lubsn  14200  ipotset  14260  ipole  14261  plusfeq  14381  pws0g  14408  frmd0  14482  symgtset  14779  oppgplusfval  14821  sylow3lem2  14939  oppglsm  14953  frgpuplem  15081  frgpupf  15082  frgpup1  15084  frgpup3lem  15086  gsumval3a  15189  gsumzoppg  15216  ablfac1eu  15308  pwsmgp  15401  opprmulfval  15407  dfrhm2  15498  subrg1  15555  staffn  15614  issrngd  15626  scafeq  15647  lbsextlem4  15914  sralem  15930  sravsca  15935  rnascl  16082  psrlinv  16142  opsrbaslem  16219  ply1scl0  16365  zlmlem  16471  zlmvsca  16476  znbaslem  16492  ipfeq  16554  thlbas  16596  thlle  16597  thloc  16599  paste  17022  ptpjcn  17305  uptx  17319  xpstopnlem1  17500  alexsubALTlem4  17744  submtmd  17787  xmetge0  17909  setsmsds  18022  tnglem  18156  tngtset  18165  tngngp2  18168  resubmet  18308  pcorev2  18526  om1plusg  18532  om1tset  18533  om1opn  18534  pi1grplem  18547  clmadd  18572  clmmul  18573  clmcj  18574  tchtopn  18657  tchnmfval  18659  bcthlem1  18746  bcthlem2  18747  bcthlem4  18749  bcth3  18753  minveclem3b  18792  pjthlem1  18801  volun  18902  voliun  18911  uniioovol  18934  itg2i1fseq  19110  itgcnlem  19144  iblabslem  19182  limcres  19236  cnplimc  19237  evlseu  19400  evl1sca  19413  mpfsubrg  19424  ply1termlem  19585  0dgr  19627  taylthlem1  19752  abelth  19817  lawcos  20114  basellem8  20325  musum  20431  chtub  20451  dchrval  20473  dchrinvcl  20492  lgsval4lem  20546  lgsquadlem2  20594  m1lgs  20601  rngoi  21047  drngoi  21074  smcnlem  21270  siii  21431  pjhthlem1  21970  dfimafnf  23041  difprsn2  23191  funcnvmptOLD  23234  funcnvmpt  23235  xpinpreima2  23291  esumid  23424  sxsigon  23523  setlikespec  24187  axlowdimlem16  24585  areacirc  24931  cbcpcp  25162  fnopabco2b  25371  ltrcmp  25405  rngounval2  25425  limhun  25570  limptlimpr2lem1  25574  supexr  25631  filnetlem4  26330  fnopabco  26388  heiborlem8  26542  mzpcompact2lem  26829  eldioph2lem1  26839  fiphp3d  26902  rmxypairf1o  26996  wopprc  27123  lmhmlnmsplit  27185  dsmmbase  27201  dsmmelbas  27205  frlmelbas  27224  islindf4  27308  psgnunilem2  27418  matbas  27468  matplusg  27469  matsca  27470  matvsca  27471  phisum  27518  dfaimafn  28027  ldualvsub  29345  dalemrotyz  29847  dalem6  29857  dalem7  29858  dalem11  29863  dalem12  29864  dalemrotps  29880  dalem30  29891  dalem35  29896  cdleme1  30416  cdleme9  30442  cdleme20c  30500  cdleme20d  30501  cdlemefrs29clN  30588  cdleme37m  30651  cdleme43aN  30678  cdlemg1b2  30760  cdlemg4f  30804  cdlemh2  31005  erngdvlem1  31177  erngdvlem2N  31178  erngdvlem3  31179  erngdvlem4  31180  erngdvlem1-rN  31185  erngdvlem2-rN  31186  erngdvlem3-rN  31187  erngdvlem4-rN  31188  dvh4dimN  31637  lcdvsub  31807  hlhilsca  32128  hlhilbase  32129  hlhilplus  32130  hlhilvsca  32140  hlhilip  32141  hlhilipval  32142
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator