Theorem syl6reqr 2527

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

Step	Hyp	Ref	Expression
1		syl6reqr.1	. 2 |- ( ph -> A = B )
2		syl6reqr.2	. . 3 |- C = B
3	2	eqcomi 2480	. 2 |- B = C
4	1, 3	syl6req 2525	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1379

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-cleq 2459

This theorem is referenced by:  iftrue  3945  iffalse  3948  difprsn1  4163  dmmptg  5502  relcoi1  5534  funimacnv  5658  resasplit  5753  dffv3  5860  dfimafn  5914  fniinfv  5924  dffv2  5938  fvco2  5940  fniunfv  6145  isoini  6220  zfrep6  6749  oprabco  6864  oeeulem  7247  ixpconstg  7475  sbthlem4  7627  sbthlem5  7628  sbthlem6  7629  supval2  7911  hartogslem1  7963  cantnflem1d  8103  cantnflem1dOLD  8126  alephsuc2  8457  dfac3  8498  xp2cda  8556  hsmexlem5  8806  axdc2lem  8824  gruima  9176  eqneg  10260  zeo  10942  fseq1p1m1  11748  hashfzo  12448  hashimarn  12458  wrdval  12513  wrdnval  12533  repswswrd  12715  s1co  12758  swrds2  12842  modfsummod  13567  telfsumo  13575  mulgcd  14039  algcvg  14060  phiprmpw  14161  strfv3  14521  resslem  14544  pwssnf1o  14749  imassca  14770  xpsfrn2  14821  homfeq  14946  oppcbas  14970  resscatc  15286  lubsn  15577  ipotset  15640  ipole  15641  plusfeq  15742  pws0g  15770  frmd0  15851  oppgplusfval  16178  symgtset  16219  gsmsymgrfix  16248  gsmsymgreq  16252  psgnunilem2  16316  sylow3lem2  16444  oppglsm  16458  frgpuplem  16586  frgpupf  16587  frgpup1  16589  frgpup3lem  16591  gsumval3aOLD  16697  gsumzoppg  16758  gsumzoppgOLD  16759  ablfac1eu  16914  pwsmgp  17051  opprmulfval  17058  dfrhm2  17150  subrg1  17222  staffn  17281  issrngd  17293  scafeq  17315  lbsextlem4  17590  sralem  17606  sravsca  17611  sraip  17612  rnascl  17763  psrlinv  17821  opsrbaslem  17913  evlseu  17956  mpfsubrg  17972  ply1scl0  18102  evl1sca  18141  evls1var  18145  zlmlem  18321  zlmvsca  18326  znbaslem  18344  ipfeq  18452  thlbas  18494  thlle  18495  thloc  18497  dsmmbase  18533  dsmmelbas  18537  frlmelbas  18555  frlmelbasOLD  18556  frlmphl  18579  islindf4  18640  matbas  18682  matplusg  18683  matsca  18684  matvsca  18685  matbas2d  18692  matsubgcell  18703  matmulcell  18714  ofco2  18720  mattposm  18728  mat1f1o  18747  mdetunilem8  18888  madugsum  18912  cramerimplem2  18953  decpmatmullem  19039  paste  19561  ptpjcn  19847  uptx  19861  xpstopnlem1  20045  alexsubALTlem4  20285  cnextf  20301  submtmd  20338  ussval  20497  tuslem  20505  psmetge0  20551  xmetge0  20582  setsmsds  20714  tnglem  20889  tngtset  20898  tngngp2  20901  resubmet  21042  pcorev2  21263  om1plusg  21269  om1tset  21270  om1opn  21271  pi1grplem  21284  clmadd  21309  clmmul  21310  clmcj  21311  tchtopn  21404  tchnmfval  21406  bcthlem1  21498  bcthlem2  21499  bcthlem4  21501  bcth3  21505  rrxmval  21567  rrxmfval  21568  ehlbase  21573  minveclem3b  21578  pjthlem1  21587  volun  21690  voliun  21699  uniioovol  21723  itg2i1fseq  21897  itgcnlem  21931  iblabslem  21969  limcres  22025  cnplimc  22026  ply1termlem  22335  0dgr  22377  taylthlem1  22502  abelth  22570  lawcos  22876  basellem8  23089  musum  23195  chtub  23215  dchrval  23237  dchrinvcl  23256  lgsval4lem  23310  lgsquadlem2  23358  m1lgs  23365  mirauto  23769  lmiisolem  23838  ttglem  23855  axlowdimlem16  23936  ebtwntg  23961  ecgrtg  23962  2pthlem2  24274  extwwlkfablem2  24755  rngoi  25058  drngoi  25085  smcnlem  25283  siii  25444  pjhthlem1  25985  sbcies  27057  imadifxp  27131  dfimafnf  27146  funcnvmptOLD  27181  funcnvmpt  27182  rdivmuldivd  27444  resvlem  27484  pstmval  27510  xpinpreima2  27525  pnfneige0  27569  zlmds  27581  zlmtset  27582  esumid  27696  sxsigon  27803  lgambdd  28219  setlikespec  28844  itg2addnclem  29643  iblabsnclem  29655  areacirc  29689  filnetlem4  29802  fnopabco  29816  heiborlem8  29917  mzpcompact2lem  30288  eldioph2lem1  30297  fiphp3d  30357  rmxypairf1o  30451  wopprc  30576  lmhmlnmsplit  30637  phisum  30764  dfaimafn  31717  ldualvsub  33952  dalemrotyz  34454  dalem6  34464  dalem7  34465  dalem11  34470  dalem12  34471  dalemrotps  34487  dalem30  34498  dalem35  34503  cdleme1  35023  cdleme9  35049  cdleme20c  35107  cdleme20d  35108  cdlemefrs29clN  35195  cdleme37m  35258  cdleme43aN  35285  cdlemg1b2  35367  cdlemg4f  35411  cdlemh2  35612  erngdvlem1  35784  erngdvlem2N  35785  erngdvlem3  35786  erngdvlem4  35787  erngdvlem1-rN  35792  erngdvlem2-rN  35793  erngdvlem3-rN  35794  erngdvlem4-rN  35795  dvh4dimN  36244  lcdvsub  36414  hlhilsca  36735  hlhilbase  36736  hlhilplus  36737  hlhilvsca  36747  hlhilip  36748  hlhilipval  36749