Theorem syl6reqr 2492

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

Syntax hints:   -> wi 4   = wceq 1364

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434

This theorem is referenced by:  iftrue  3794  iffalse  3796  difprsn1  4007  dmmptg  5332  relcoi1  5363  funimacnv  5487  resasplit  5578  dffv3  5684  dfimafn  5737  fniinfv  5747  dffv2  5761  fvco2  5763  fniunfv  5961  isoini  6026  zfrep6  6544  oprabco  6656  oeeulem  7036  ixpconstg  7268  sbthlem4  7420  sbthlem5  7421  sbthlem6  7422  supval2  7701  hartogslem1  7752  cantnflem1d  7892  cantnflem1dOLD  7915  alephsuc2  8246  dfac3  8287  xp2cda  8345  hsmexlem5  8595  axdc2lem  8613  gruima  8965  eqneg  10047  zeo  10723  fseq1p1m1  11530  hashfzo  12186  hashimarn  12196  wrdval  12234  repswswrd  12418  s1co  12457  swrds2  12541  fsumtscopo  13261  mulgcd  13726  algcvg  13747  phiprmpw  13847  strfv3  14205  resslem  14227  pwssnf1o  14432  imassca  14453  xpsfrn2  14504  homfeq  14629  oppcbas  14653  resscatc  14969  lubsn  15260  ipotset  15323  ipole  15324  plusfeq  15425  pws0g  15453  frmd0  15531  oppgplusfval  15856  symgtset  15897  gsmsymgrfix  15926  gsmsymgreq  15930  psgnunilem2  15994  sylow3lem2  16120  oppglsm  16134  frgpuplem  16262  frgpupf  16263  frgpup1  16265  frgpup3lem  16267  gsumval3aOLD  16373  gsumzoppg  16432  gsumzoppgOLD  16433  ablfac1eu  16564  pwsmgp  16700  opprmulfval  16707  dfrhm2  16798  subrg1  16855  staffn  16914  issrngd  16926  scafeq  16948  lbsextlem4  17220  sralem  17236  sravsca  17241  sraip  17242  rnascl  17391  psrlinv  17446  opsrbaslem  17535  evlseu  17578  mpfsubrg  17594  ply1scl0  17717  evl1sca  17737  evls1var  17741  zlmlem  17907  zlmvsca  17912  znbaslem  17930  ipfeq  18038  thlbas  18080  thlle  18081  thloc  18083  dsmmbase  18119  dsmmelbas  18123  frlmelbas  18141  frlmelbasOLD  18142  frlmphl  18165  islindf4  18226  matbas  18273  matplusg  18274  matsca  18275  matvsca  18276  matbas2d  18283  ofco2  18291  mattposm  18303  mdetunilem8  18384  madugsum  18408  cramerimplem2  18449  paste  18857  ptpjcn  19143  uptx  19157  xpstopnlem1  19341  alexsubALTlem4  19581  cnextf  19597  submtmd  19634  ussval  19793  tuslem  19801  psmetge0  19847  xmetge0  19878  setsmsds  20010  tnglem  20185  tngtset  20194  tngngp2  20197  resubmet  20338  pcorev2  20559  om1plusg  20565  om1tset  20566  om1opn  20567  pi1grplem  20580  clmadd  20605  clmmul  20606  clmcj  20607  tchtopn  20700  tchnmfval  20702  bcthlem1  20794  bcthlem2  20795  bcthlem4  20797  bcth3  20801  rrxmval  20863  rrxmfval  20864  ehlbase  20869  minveclem3b  20874  pjthlem1  20883  volun  20985  voliun  20994  uniioovol  21018  itg2i1fseq  21192  itgcnlem  21226  iblabslem  21264  limcres  21320  cnplimc  21321  ply1termlem  21630  0dgr  21672  taylthlem1  21797  abelth  21865  lawcos  22171  basellem8  22384  musum  22490  chtub  22510  dchrval  22532  dchrinvcl  22551  lgsval4lem  22605  lgsquadlem2  22653  m1lgs  22660  mirauto  23027  ttglem  23057  axlowdimlem16  23138  ebtwntg  23163  ecgrtg  23164  2pthlem2  23430  rngoi  23802  drngoi  23829  smcnlem  24027  siii  24188  pjhthlem1  24729  sbcies  25801  imadifxp  25874  dfimafnf  25885  funcnvmptOLD  25921  funcnvmpt  25922  rdivmuldivd  26194  resvlem  26235  pstmval  26258  xpinpreima2  26273  pnfneige0  26317  zlmds  26329  zlmtset  26330  esumid  26435  sxsigon  26542  lgambdd  26953  setlikespec  27577  itg2addnclem  28368  iblabsnclem  28380  areacirc  28414  filnetlem4  28527  fnopabco  28541  heiborlem8  28642  mzpcompact2lem  29013  eldioph2lem1  29023  fiphp3d  29083  rmxypairf1o  29177  wopprc  29304  lmhmlnmsplit  29365  phisum  29492  dfaimafn  29996  modfsummod  30170  wrdnval  30399  extwwlkfablem2  30596  matsubgcell  30744  ldualvsub  32522  dalemrotyz  33024  dalem6  33034  dalem7  33035  dalem11  33040  dalem12  33041  dalemrotps  33057  dalem30  33068  dalem35  33073  cdleme1  33593  cdleme9  33619  cdleme20c  33677  cdleme20d  33678  cdlemefrs29clN  33765  cdleme37m  33828  cdleme43aN  33855  cdlemg1b2  33937  cdlemg4f  33981  cdlemh2  34182  erngdvlem1  34354  erngdvlem2N  34355  erngdvlem3  34356  erngdvlem4  34357  erngdvlem1-rN  34362  erngdvlem2-rN  34363  erngdvlem3-rN  34364  erngdvlem4-rN  34365  dvh4dimN  34814  lcdvsub  34984  hlhilsca  35305  hlhilbase  35306  hlhilplus  35307  hlhilvsca  35317  hlhilip  35318  hlhilipval  35319