Theorem syl6reqr 2489

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

Syntax hints:   -> wi 4   = wceq 1437

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-cleq 2421

This theorem is referenced by:  iftrue  3921  iffalse  3924  difprsn1  4139  dmmptg  5352  relcoi1OLD  5385  setlikespec  5420  funimacnv  5673  dmmptd  5726  resasplit  5770  dffv3  5877  dfimafn  5930  fniinfv  5940  dffv2  5954  fvco2  5956  fniunfv  6167  isoini  6244  zfrep6  6775  oprabco  6891  oeeulem  7310  ixpconstg  7539  sbthlem4  7691  sbthlem5  7692  sbthlem6  7693  supval2  7975  hartogslem1  8057  cantnflem1d  8192  alephsuc2  8509  dfac3  8550  xp2cda  8608  hsmexlem5  8858  axdc2lem  8876  gruima  9226  eqneg  10326  zeo  11021  fseq1p1m1  11866  hashfzo  12596  hashimarn  12605  wrdval  12661  wrdnval  12684  repswswrd  12872  s1co  12915  swrds2  12999  modfsummod  13832  telfsumo  13840  mulgcd  14485  algcvg  14506  phiprmpw  14693  strfv3  15121  resslem  15144  pwssnf1o  15355  imassca  15376  xpsfrn2  15427  homfeq  15550  oppcbas  15574  resscatc  15951  estrcbasbas  15967  funcestrcsetclem7  15982  funcestrcsetclem8  15983  funcestrcsetclem9  15984  fthestrcsetc  15986  fullestrcsetc  15987  equivestrcsetc  15988  setc1strwun  15989  funcsetcestrclem7  15997  funcsetcestrclem8  15998  funcsetcestrclem9  15999  fthsetcestrc  16001  fullsetcestrc  16002  lubsn  16291  ipotset  16354  ipole  16355  plusfeq  16446  pws0g  16523  frmd0  16595  oppgplusfval  16950  symgtset  16991  gsmsymgrfix  17020  gsmsymgreq  17024  psgnunilem2  17087  sylow3lem2  17215  oppglsm  17229  frgpuplem  17357  frgpupf  17358  frgpup1  17360  frgpup3lem  17362  gsumzoppg  17512  ablfac1eu  17641  pwsmgp  17781  opprmulfval  17788  dfrhm2  17880  subrg1  17953  staffn  18012  issrngd  18024  scafeq  18046  lbsextlem4  18319  sralem  18335  sravsca  18340  sraip  18341  rnascl  18502  psrlinv  18556  opsrbaslem  18636  evlseu  18674  mpfsubrg  18690  ply1scl0  18818  evl1sca  18857  evls1var  18861  zlmlem  19019  zlmvsca  19024  znbaslem  19040  ipfeq  19148  thlbas  19190  thlle  19191  thloc  19193  dsmmbase  19229  dsmmelbas  19233  frlmelbas  19250  frlmphl  19270  islindf4  19327  matbas  19369  matplusg  19370  matsca  19371  matvsca  19372  matbas2d  19379  matsubgcell  19390  matmulcell  19401  ofco2  19407  mattposm  19415  mat1f1o  19434  mdetunilem8  19575  madugsum  19599  cramerimplem2  19640  decpmatmullem  19726  paste  20241  ptpjcn  20557  uptx  20571  xpstopnlem1  20755  alexsubALTlem4  20996  cnextf  21012  submtmd  21050  ussval  21205  tuslem  21213  psmetge0  21259  xmetge0  21290  setsmsds  21422  tnglem  21579  tngtset  21588  tngngp2  21591  resubmet  21731  pcorev2  21952  om1plusg  21958  om1tset  21959  om1opn  21960  pi1grplem  21973  clmadd  21998  clmmul  21999  clmcj  22000  tchtopn  22093  tchnmfval  22095  bcthlem1  22185  bcthlem2  22186  bcthlem4  22188  bcth3  22192  rrxmval  22252  rrxmfval  22253  ehlbase  22258  minveclem3b  22263  pjthlem1  22272  volun  22375  voliun  22384  uniioovol  22413  itg2i1fseq  22590  itgcnlem  22624  iblabslem  22662  limcres  22718  cnplimc  22719  ply1termlem  23025  0dgr  23067  taylthlem1  23193  abelth  23261  lawcos  23610  lgambdd  23827  basellem8  23877  musum  23983  chtub  24003  dchrval  24025  dchrinvcl  24044  lgsval4lem  24098  lgsquadlem2  24146  m1lgs  24153  mirauto  24586  lmiisolem  24694  ttglem  24752  axlowdimlem16  24833  ebtwntg  24858  ecgrtg  24859  2pthlem2  25171  extwwlkfablem2  25651  rngoi  25953  drngoi  25980  smcnlem  26178  siii  26339  pjhthlem1  26879  sbcies  27953  imadifxp  28051  dfimafnf  28073  funcnvmptOLD  28110  funcnvmpt  28111  rdivmuldivd  28393  resvlem  28433  mdetpmtr12  28490  pstmval  28537  xpinpreima2  28552  pnfneige0  28596  zlmds  28607  zlmtset  28608  esumid  28704  esumrnmpt  28712  sxsigon  28853  carsgclctunlem1  28978  filnetlem4  30822  itg2addnclem  31697  iblabsnclem  31709  areacirc  31741  fnopabco  31753  heiborlem8  31854  ldualvsub  32430  dalemrotyz  32932  dalem6  32942  dalem7  32943  dalem11  32948  dalem12  32949  dalemrotps  32965  dalem30  32976  dalem35  32981  cdleme1  33502  cdleme9  33528  cdleme20c  33587  cdleme20d  33588  cdlemefrs29clN  33675  cdleme37m  33738  cdleme43aN  33765  cdlemg1b2  33847  cdlemg4f  33891  cdlemh2  34092  erngdvlem1  34264  erngdvlem2N  34265  erngdvlem3  34266  erngdvlem4  34267  erngdvlem1-rN  34272  erngdvlem2-rN  34273  erngdvlem3-rN  34274  erngdvlem4-rN  34275  dvh4dimN  34724  lcdvsub  34894  hlhilsca  35215  hlhilbase  35216  hlhilplus  35217  hlhilvsca  35227  hlhilip  35228  hlhilipval  35229  mzpcompact2lem  35302  eldioph2lem1  35311  fiphp3d  35371  rmxypairf1o  35465  wopprc  35591  lmhmlnmsplit  35651  phisum  35775  ellimcabssub0  37269  cosknegpi  37316  fourierdlem58  37596  fourierdlem59  37597  fourierdlem72  37610  fourierdlem80  37618  sqwvfourb  37661  etransclem28  37694  etransclem41  37707  dfaimafn  38057