Theorem syl6reqr 2503

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

Syntax hints:   -> wi 4   = wceq 1383

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421

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

This theorem is referenced by:  iftrue  3932  iffalse  3935  difprsn1  4151  dmmptg  5494  relcoi1  5526  funimacnv  5650  dmmptd  5701  resasplit  5745  dffv3  5852  dfimafn  5907  fniinfv  5917  dffv2  5931  fvco2  5933  fniunfv  6144  isoini  6219  zfrep6  6753  oprabco  6869  oeeulem  7252  ixpconstg  7480  sbthlem4  7632  sbthlem5  7633  sbthlem6  7634  supval2  7917  hartogslem1  7970  cantnflem1d  8110  cantnflem1dOLD  8133  alephsuc2  8464  dfac3  8505  xp2cda  8563  hsmexlem5  8813  axdc2lem  8831  gruima  9183  eqneg  10270  zeo  10954  fseq1p1m1  11761  hashfzo  12466  hashimarn  12475  wrdval  12530  wrdnval  12550  repswswrd  12735  s1co  12778  swrds2  12862  modfsummod  13587  telfsumo  13595  mulgcd  14061  algcvg  14082  phiprmpw  14183  strfv3  14544  resslem  14567  pwssnf1o  14772  imassca  14793  xpsfrn2  14844  homfeq  14966  oppcbas  14990  resscatc  15306  lubsn  15598  ipotset  15661  ipole  15662  plusfeq  15753  pws0g  15830  frmd0  15902  oppgplusfval  16257  symgtset  16298  gsmsymgrfix  16327  gsmsymgreq  16331  psgnunilem2  16394  sylow3lem2  16522  oppglsm  16536  frgpuplem  16664  frgpupf  16665  frgpup1  16667  frgpup3lem  16669  gsumval3aOLD  16780  gsumzoppg  16841  gsumzoppgOLD  16842  ablfac1eu  16998  pwsmgp  17141  opprmulfval  17148  dfrhm2  17240  subrg1  17313  staffn  17372  issrngd  17384  scafeq  17406  lbsextlem4  17681  sralem  17697  sravsca  17702  sraip  17703  rnascl  17866  psrlinv  17924  opsrbaslem  18016  evlseu  18059  mpfsubrg  18075  ply1scl0  18205  evl1sca  18244  evls1var  18248  zlmlem  18427  zlmvsca  18432  znbaslem  18450  ipfeq  18558  thlbas  18600  thlle  18601  thloc  18603  dsmmbase  18639  dsmmelbas  18643  frlmelbas  18661  frlmelbasOLD  18662  frlmphl  18685  islindf4  18746  matbas  18788  matplusg  18789  matsca  18790  matvsca  18791  matbas2d  18798  matsubgcell  18809  matmulcell  18820  ofco2  18826  mattposm  18834  mat1f1o  18853  mdetunilem8  18994  madugsum  19018  cramerimplem2  19059  decpmatmullem  19145  paste  19668  ptpjcn  19985  uptx  19999  xpstopnlem1  20183  alexsubALTlem4  20423  cnextf  20439  submtmd  20476  ussval  20635  tuslem  20643  psmetge0  20689  xmetge0  20720  setsmsds  20852  tnglem  21027  tngtset  21036  tngngp2  21039  resubmet  21180  pcorev2  21401  om1plusg  21407  om1tset  21408  om1opn  21409  pi1grplem  21422  clmadd  21447  clmmul  21448  clmcj  21449  tchtopn  21542  tchnmfval  21544  bcthlem1  21636  bcthlem2  21637  bcthlem4  21639  bcth3  21643  rrxmval  21705  rrxmfval  21706  ehlbase  21711  minveclem3b  21716  pjthlem1  21725  volun  21828  voliun  21837  uniioovol  21861  itg2i1fseq  22035  itgcnlem  22069  iblabslem  22107  limcres  22163  cnplimc  22164  ply1termlem  22473  0dgr  22515  taylthlem1  22640  abelth  22708  lawcos  23020  basellem8  23233  musum  23339  chtub  23359  dchrval  23381  dchrinvcl  23400  lgsval4lem  23454  lgsquadlem2  23502  m1lgs  23509  mirauto  23933  lmiisolem  24033  ttglem  24051  axlowdimlem16  24132  ebtwntg  24157  ecgrtg  24158  2pthlem2  24470  extwwlkfablem2  24950  rngoi  25254  drngoi  25281  smcnlem  25479  siii  25640  pjhthlem1  26181  sbcies  27253  imadifxp  27330  dfimafnf  27345  funcnvmptOLD  27381  funcnvmpt  27382  rdivmuldivd  27654  resvlem  27694  pstmval  27747  xpinpreima2  27762  pnfneige0  27806  zlmds  27818  zlmtset  27819  esumid  27929  sxsigon  28036  lgambdd  28452  setlikespec  29242  itg2addnclem  30041  iblabsnclem  30053  areacirc  30087  filnetlem4  30174  fnopabco  30188  heiborlem8  30289  mzpcompact2lem  30659  eldioph2lem1  30668  fiphp3d  30728  rmxypairf1o  30822  wopprc  30947  lmhmlnmsplit  31008  phisum  31135  ellimcabssub0  31531  cosknegpi  31576  fourierdlem58  31836  fourierdlem59  31837  fourierdlem72  31850  fourierdlem80  31858  sqwvfourb  31901  dfaimafn  32088  estrcbasbas  32486  funcestrcsetclem7  32501  funcestrcsetclem8  32502  funcestrcsetclem9  32503  ldualvsub  34620  dalemrotyz  35122  dalem6  35132  dalem7  35133  dalem11  35138  dalem12  35139  dalemrotps  35155  dalem30  35166  dalem35  35171  cdleme1  35692  cdleme9  35718  cdleme20c  35777  cdleme20d  35778  cdlemefrs29clN  35865  cdleme37m  35928  cdleme43aN  35955  cdlemg1b2  36037  cdlemg4f  36081  cdlemh2  36282  erngdvlem1  36454  erngdvlem2N  36455  erngdvlem3  36456  erngdvlem4  36457  erngdvlem1-rN  36462  erngdvlem2-rN  36463  erngdvlem3-rN  36464  erngdvlem4-rN  36465  dvh4dimN  36914  lcdvsub  37084  hlhilsca  37405  hlhilbase  37406  hlhilplus  37407  hlhilvsca  37417  hlhilip  37418  hlhilipval  37419