Theorem syl6reqr 2514

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

Syntax hints:   -> wi 4   = wceq 1398

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432

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

This theorem is referenced by:  iftrue  3935  iffalse  3938  difprsn1  4152  dmmptg  5487  relcoi1  5519  funimacnv  5642  dmmptd  5693  resasplit  5737  dffv3  5844  dfimafn  5897  fniinfv  5907  dffv2  5921  fvco2  5923  fniunfv  6134  isoini  6209  zfrep6  6741  oprabco  6857  oeeulem  7242  ixpconstg  7471  sbthlem4  7623  sbthlem5  7624  sbthlem6  7625  supval2  7906  hartogslem1  7959  cantnflem1d  8098  cantnflem1dOLD  8121  alephsuc2  8452  dfac3  8493  xp2cda  8551  hsmexlem5  8801  axdc2lem  8819  gruima  9169  eqneg  10260  zeo  10944  fseq1p1m1  11756  hashfzo  12471  hashimarn  12480  wrdval  12536  wrdnval  12559  repswswrd  12747  s1co  12790  swrds2  12874  modfsummod  13690  telfsumo  13698  mulgcd  14268  algcvg  14289  phiprmpw  14390  strfv3  14753  resslem  14776  pwssnf1o  14987  imassca  15008  xpsfrn2  15059  homfeq  15182  oppcbas  15206  resscatc  15583  estrcbasbas  15599  funcestrcsetclem7  15614  funcestrcsetclem8  15615  funcestrcsetclem9  15616  fthestrcsetc  15618  fullestrcsetc  15619  equivestrcsetc  15620  setc1strwun  15621  funcsetcestrclem7  15629  funcsetcestrclem8  15630  funcsetcestrclem9  15631  fthsetcestrc  15633  fullsetcestrc  15634  lubsn  15923  ipotset  15986  ipole  15987  plusfeq  16078  pws0g  16155  frmd0  16227  oppgplusfval  16582  symgtset  16623  gsmsymgrfix  16652  gsmsymgreq  16656  psgnunilem2  16719  sylow3lem2  16847  oppglsm  16861  frgpuplem  16989  frgpupf  16990  frgpup1  16992  frgpup3lem  16994  gsumval3aOLD  17105  gsumzoppg  17165  gsumzoppgOLD  17166  ablfac1eu  17319  pwsmgp  17462  opprmulfval  17469  dfrhm2  17561  subrg1  17634  staffn  17693  issrngd  17705  scafeq  17727  lbsextlem4  18002  sralem  18018  sravsca  18023  sraip  18024  rnascl  18187  psrlinv  18245  opsrbaslem  18337  evlseu  18380  mpfsubrg  18396  ply1scl0  18526  evl1sca  18565  evls1var  18569  zlmlem  18729  zlmvsca  18734  znbaslem  18750  ipfeq  18858  thlbas  18900  thlle  18901  thloc  18903  dsmmbase  18939  dsmmelbas  18943  frlmelbas  18961  frlmphl  18983  islindf4  19040  matbas  19082  matplusg  19083  matsca  19084  matvsca  19085  matbas2d  19092  matsubgcell  19103  matmulcell  19114  ofco2  19120  mattposm  19128  mat1f1o  19147  mdetunilem8  19288  madugsum  19312  cramerimplem2  19353  decpmatmullem  19439  paste  19962  ptpjcn  20278  uptx  20292  xpstopnlem1  20476  alexsubALTlem4  20716  cnextf  20732  submtmd  20769  ussval  20928  tuslem  20936  psmetge0  20982  xmetge0  21013  setsmsds  21145  tnglem  21320  tngtset  21329  tngngp2  21332  resubmet  21473  pcorev2  21694  om1plusg  21700  om1tset  21701  om1opn  21702  pi1grplem  21715  clmadd  21740  clmmul  21741  clmcj  21742  tchtopn  21835  tchnmfval  21837  bcthlem1  21929  bcthlem2  21930  bcthlem4  21932  bcth3  21936  rrxmval  21998  rrxmfval  21999  ehlbase  22004  minveclem3b  22009  pjthlem1  22018  volun  22121  voliun  22130  uniioovol  22154  itg2i1fseq  22328  itgcnlem  22362  iblabslem  22400  limcres  22456  cnplimc  22457  ply1termlem  22766  0dgr  22808  taylthlem1  22934  abelth  23002  lawcos  23347  basellem8  23559  musum  23665  chtub  23685  dchrval  23707  dchrinvcl  23726  lgsval4lem  23780  lgsquadlem2  23828  m1lgs  23835  mirauto  24262  lmiisolem  24362  ttglem  24381  axlowdimlem16  24462  ebtwntg  24487  ecgrtg  24488  2pthlem2  24800  extwwlkfablem2  25280  rngoi  25580  drngoi  25607  smcnlem  25805  siii  25966  pjhthlem1  26507  sbcies  27579  imadifxp  27672  dfimafnf  27694  funcnvmptOLD  27736  funcnvmpt  27737  rdivmuldivd  28016  resvlem  28056  pstmval  28109  xpinpreima2  28124  pnfneige0  28168  zlmds  28179  zlmtset  28180  esumid  28273  esumrnmpt  28281  sxsigon  28400  carsgclctunlem1  28525  lgambdd  28843  setlikespec  29507  itg2addnclem  30306  iblabsnclem  30318  areacirc  30352  filnetlem4  30439  fnopabco  30453  heiborlem8  30554  mzpcompact2lem  30923  eldioph2lem1  30932  fiphp3d  30992  rmxypairf1o  31086  wopprc  31211  lmhmlnmsplit  31272  phisum  31400  ellimcabssub0  31862  cosknegpi  31908  fourierdlem58  32186  fourierdlem59  32187  fourierdlem72  32200  fourierdlem80  32208  sqwvfourb  32251  etransclem28  32284  etransclem41  32297  dfaimafn  32489  ldualvsub  35277  dalemrotyz  35779  dalem6  35789  dalem7  35790  dalem11  35795  dalem12  35796  dalemrotps  35812  dalem30  35823  dalem35  35828  cdleme1  36349  cdleme9  36375  cdleme20c  36434  cdleme20d  36435  cdlemefrs29clN  36522  cdleme37m  36585  cdleme43aN  36612  cdlemg1b2  36694  cdlemg4f  36738  cdlemh2  36939  erngdvlem1  37111  erngdvlem2N  37112  erngdvlem3  37113  erngdvlem4  37114  erngdvlem1-rN  37119  erngdvlem2-rN  37120  erngdvlem3-rN  37121  erngdvlem4-rN  37122  dvh4dimN  37571  lcdvsub  37741  hlhilsca  38062  hlhilbase  38063  hlhilplus  38064  hlhilvsca  38074  hlhilip  38075  hlhilipval  38076