Theorem syl6reqr 2515

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 2471	. 2 |- B = C
4	1, 3	syl6req 2513	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1455

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-ext 2442

This theorem depends on definitions:  df-bi 190  df-cleq 2455

This theorem is referenced by:  iftrue  3899  iffalse  3902  difprsn1  4121  dmmptg  5351  relcoi1OLD  5384  setlikespec  5420  funimacnv  5677  dmmptd  5730  resasplit  5776  dffv3  5884  dfimafn  5937  fniinfv  5947  dffv2  5961  fvco2  5963  fniunfv  6177  isoini  6254  zfrep6  6788  oprabco  6907  oeeulem  7328  ixpconstg  7557  sbthlem4  7711  sbthlem5  7712  sbthlem6  7713  supval2  7995  hartogslem1  8083  cantnflem1d  8219  alephsuc2  8537  dfac3  8578  xp2cda  8636  hsmexlem5  8886  axdc2lem  8904  gruima  9253  eqneg  10355  zeo  11050  fseq1p1m1  11897  hashfzo  12634  hashimarn  12643  wrdval  12707  wrdnval  12733  repswswrd  12924  s1co  12967  swrds2  13066  modfsummod  13903  telfsumo  13911  mulgcd  14563  algcvg  14584  phiprmpw  14773  strfv3  15207  resslem  15231  pwssnf1o  15445  imassca  15469  xpsfrn2  15525  homfeq  15648  oppcbas  15672  resscatc  16049  estrcbasbas  16065  funcestrcsetclem7  16080  funcestrcsetclem8  16081  funcestrcsetclem9  16082  fthestrcsetc  16084  fullestrcsetc  16085  equivestrcsetc  16086  setc1strwun  16087  funcsetcestrclem7  16095  funcsetcestrclem8  16096  funcsetcestrclem9  16097  fthsetcestrc  16099  fullsetcestrc  16100  lubsn  16389  ipotset  16452  ipole  16453  plusfeq  16544  pws0g  16621  frmd0  16693  oppgplusfval  17048  symgtset  17089  gsmsymgrfix  17118  gsmsymgreq  17122  psgnunilem2  17185  sylow3lem2  17329  oppglsm  17343  frgpuplem  17471  frgpupf  17472  frgpup1  17474  frgpup3lem  17476  gsumzoppg  17626  ablfac1eu  17755  pwsmgp  17895  opprmulfval  17902  dfrhm2  17994  subrg1  18067  staffn  18126  issrngd  18138  scafeq  18160  lbsextlem4  18433  sralem  18449  sravsca  18454  sraip  18455  rnascl  18616  psrlinv  18670  opsrbaslem  18750  evlseu  18788  mpfsubrg  18804  ply1scl0  18932  evl1sca  18971  evls1var  18975  zlmlem  19137  zlmvsca  19142  znbaslem  19158  ipfeq  19266  thlbas  19308  thlle  19309  thloc  19311  dsmmbase  19347  dsmmelbas  19351  frlmelbas  19368  frlmphl  19388  islindf4  19445  matbas  19487  matplusg  19488  matsca  19489  matvsca  19490  matbas2d  19497  matsubgcell  19508  matmulcell  19519  ofco2  19525  mattposm  19533  mat1f1o  19552  mdetunilem8  19693  madugsum  19717  cramerimplem2  19758  decpmatmullem  19844  paste  20359  ptpjcn  20675  uptx  20689  xpstopnlem1  20873  alexsubALTlem4  21114  cnextf  21130  submtmd  21168  ussval  21323  tuslem  21331  psmetge0  21377  xmetge0  21408  setsmsds  21540  tnglem  21697  tngtset  21706  tngngp2  21709  resubmet  21869  pcorev2  22108  om1plusg  22114  om1tset  22115  om1opn  22116  pi1grplem  22129  clmadd  22154  clmmul  22155  clmcj  22156  tchtopn  22249  tchnmfval  22251  bcthlem1  22341  bcthlem2  22342  bcthlem4  22344  bcth3  22348  rrxmval  22408  rrxmfval  22409  ehlbase  22414  minveclem3b  22419  minveclem3bOLD  22431  pjthlem1  22440  volun  22547  voliun  22556  uniioovol  22585  itg2i1fseq  22762  itgcnlem  22796  iblabslem  22834  limcres  22890  cnplimc  22891  ply1termlem  23206  0dgr  23248  taylthlem1  23377  abelth  23445  lawcos  23794  lgambdd  24011  basellem8  24063  musum  24169  chtub  24189  dchrval  24211  dchrinvcl  24230  lgsval4lem  24284  lgsquadlem2  24332  m1lgs  24339  mirauto  24778  lmiisolem  24887  ttglem  24955  axlowdimlem16  25036  ebtwntg  25061  ecgrtg  25062  2pthlem2  25375  extwwlkfablem2  25855  rngoi  26157  drngoi  26184  smcnlem  26382  siii  26543  pjhthlem1  27093  sbcies  28167  imadifxp  28261  dfimafnf  28282  funcnvmptOLD  28319  funcnvmpt  28320  rdivmuldivd  28603  resvlem  28643  mdetpmtr12  28700  pstmval  28747  xpinpreima2  28762  pnfneige0  28806  zlmds  28817  zlmtset  28818  esumid  28914  esumrnmpt  28922  sxsigon  29063  carsgclctunlem1  29198  filnetlem4  31086  finxpreclem4  31831  itg2addnclem  32038  iblabsnclem  32050  areacirc  32082  fnopabco  32094  heiborlem8  32195  ldualvsub  32766  dalemrotyz  33268  dalem6  33278  dalem7  33279  dalem11  33284  dalem12  33285  dalemrotps  33301  dalem30  33312  dalem35  33317  cdleme1  33838  cdleme9  33864  cdleme20c  33923  cdleme20d  33924  cdlemefrs29clN  34011  cdleme37m  34074  cdleme43aN  34101  cdlemg1b2  34183  cdlemg4f  34227  cdlemh2  34428  erngdvlem1  34600  erngdvlem2N  34601  erngdvlem3  34602  erngdvlem4  34603  erngdvlem1-rN  34608  erngdvlem2-rN  34609  erngdvlem3-rN  34610  erngdvlem4-rN  34611  dvh4dimN  35060  lcdvsub  35230  hlhilsca  35551  hlhilbase  35552  hlhilplus  35553  hlhilvsca  35563  hlhilip  35564  hlhilipval  35565  mzpcompact2lem  35638  eldioph2lem1  35647  fiphp3d  35707  rmxypairf1o  35804  wopprc  35930  lmhmlnmsplit  35990  phisum  36121  clcnvlem  36275  ellimcabssub0  37735  cosknegpi  37782  fourierdlem58  38066  fourierdlem59  38067  fourierdlem72  38080  fourierdlem80  38088  sqwvfourb  38131  etransclem28  38165  etransclem41  38178  dfaimafn  38705  funsneqopsn  39065  uspgrf1oedg  39308  nbgrval  39456