Theorem syl6reqr 2675

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

Syntax hints:   -> wi 4   = wceq 1483

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1705  df-cleq 2615

This theorem is referenced by:  iftrue  4092  iffalse  4095  difprsn1  4330  dmmptg  5632  setlikespec  5701  funimacnv  5970  dmmptd  6024  resasplit  6074  dffv3  6187  dfimafn  6245  fniinfv  6257  dffv2  6271  fvco2  6273  funsneqopsn  6417  fniunfv  6505  isoini  6588  zfrep6  7134  oprabco  7261  oeeulem  7681  ixpconstg  7917  sbthlem4  8073  sbthlem5  8074  sbthlem6  8075  supval2  8361  hartogslem1  8447  cantnflem1d  8585  alephsuc2  8903  dfac3  8944  xp2cda  9002  hsmexlem5  9252  axdc2lem  9270  gruima  9624  eqneg  10745  zeo  11463  fseq1p1m1  12414  hashfzo  13216  hashimarn  13227  wrdval  13308  wrdnval  13335  repswswrd  13531  s1co  13579  swrds2  13685  modfsummod  14526  telfsumo  14534  mulgcd  15265  algcvg  15289  phiprmpw  15481  phisum  15495  strfv3  15908  resslem  15933  pwssnf1o  16158  imassca  16179  xpsfrn2  16230  homfeq  16354  oppcbas  16378  resscatc  16755  estrcbasbas  16771  funcestrcsetclem7  16786  funcestrcsetclem8  16787  funcestrcsetclem9  16788  fthestrcsetc  16790  fullestrcsetc  16791  equivestrcsetc  16792  setc1strwun  16793  funcsetcestrclem7  16801  funcsetcestrclem8  16802  funcsetcestrclem9  16803  fthsetcestrc  16805  fullsetcestrc  16806  lubsn  17094  ipotset  17157  ipole  17158  plusfeq  17249  pws0g  17326  frmd0  17397  oppgplusfval  17778  symgtset  17819  gsmsymgrfix  17848  gsmsymgreq  17852  psgnunilem2  17915  sylow3lem2  18043  oppglsm  18057  frgpuplem  18185  frgpupf  18186  frgpup1  18188  frgpup3lem  18190  gsumzoppg  18344  ablfac1eu  18472  pwsmgp  18618  opprmulfval  18625  dfrhm2  18717  subrg1  18790  staffn  18849  issrngd  18861  scafeq  18883  lbsextlem4  19161  sralem  19177  sravsca  19182  sraip  19183  rnascl  19343  psrlinv  19397  opsrbaslem  19477  opsrbaslemOLD  19478  evlseu  19516  mpfsubrg  19532  ply1scl0  19660  evl1sca  19698  evls1var  19702  zlmlem  19865  zlmvsca  19870  znbaslem  19886  znbaslemOLD  19887  ipfeq  19995  ssipeq  20001  thlbas  20040  thlle  20041  thloc  20043  dsmmbase  20079  dsmmelbas  20083  frlmelbas  20100  frlmphl  20120  islindf4  20177  matbas  20219  matplusg  20220  matsca  20221  matvsca  20222  matbas2d  20229  matsubgcell  20240  matmulcell  20251  ofco2  20257  mattposm  20265  mat1f1o  20284  mdetunilem8  20425  madugsum  20449  cramerimplem2  20490  decpmatmullem  20576  paste  21098  ptpjcn  21414  uptx  21428  xpstopnlem1  21612  alexsubALTlem4  21854  cnextf  21870  submtmd  21908  ussval  22063  tuslem  22071  psmetge0  22117  xmetge0  22149  setsmsds  22281  sgrim  22435  tnglem  22444  tngtset  22453  tngngp2  22456  resubmet  22605  pcorev2  22828  om1plusg  22834  om1tset  22835  om1opn  22836  pi1grplem  22849  clmadd  22874  clmmul  22875  clmcj  22876  tchtopn  23025  tchnmfval  23027  bcthlem1  23121  bcthlem2  23122  bcthlem4  23124  bcth3  23128  rrxmval  23188  rrxmfval  23189  ehlbase  23194  minveclem3b  23199  pjthlem1  23208  volun  23313  voliun  23322  uniioovol  23347  itg2i1fseq  23522  itgcnlem  23556  iblabslem  23594  limcres  23650  cnplimc  23651  ply1termlem  23959  0dgr  24001  taylthlem1  24127  abelth  24195  lawcos  24546  lgambdd  24763  basellem8  24814  musum  24917  chtub  24937  dchrval  24959  dchrinvcl  24978  lgsval4lem  25033  lgsquadlem2  25106  m1lgs  25113  mirauto  25579  lmiisolem  25688  ttglem  25756  axlowdimlem16  25837  ebtwntg  25862  ecgrtg  25863  nbgrval  26234  uvtxupgrres  26309  eucrct2eupth  27105  smcnlem  27552  siii  27708  pjhthlem1  28250  sbcies  29322  imadifxp  29414  dfimafnf  29436  funcnvmptOLD  29467  funcnvmpt  29468  rdivmuldivd  29791  resvlem  29831  mdetpmtr12  29891  pstmval  29938  xpinpreima2  29953  pnfneige0  29997  zlmds  30008  zlmtset  30009  esumid  30106  esumrnmpt  30114  sxsigon  30255  carsgclctunlem1  30379  circlemethnat  30719  filnetlem4  32376  finxpreclem4  33231  itg2addnclem  33461  iblabsnclem  33473  areacirc  33505  fnopabco  33517  heiborlem8  33617  rngoi  33698  drngoi  33750  ldualvsub  34442  dalemrotyz  34944  dalem6  34954  dalem7  34955  dalem11  34960  dalem12  34961  dalemrotps  34977  dalem30  34988  dalem35  34993  cdleme1  35514  cdleme9  35540  cdleme20c  35599  cdleme20d  35600  cdlemefrs29clN  35687  cdleme37m  35750  cdleme43aN  35777  cdlemg1b2  35859  cdlemg4f  35903  cdlemh2  36104  erngdvlem1  36276  erngdvlem2N  36277  erngdvlem3  36278  erngdvlem4  36279  erngdvlem1-rN  36284  erngdvlem2-rN  36285  erngdvlem3-rN  36286  erngdvlem4-rN  36287  dvh4dimN  36736  lcdvsub  36906  hlhilsca  37227  hlhilbase  37228  hlhilplus  37229  hlhilvsca  37239  hlhilip  37240  hlhilipval  37241  mzpcompact2lem  37314  eldioph2lem1  37323  fiphp3d  37383  rmxypairf1o  37476  wopprc  37597  lmhmlnmsplit  37657  clcnvlem  37930  dmmptdf  39417  dmmptdf2  39439  ellimcabssub0  39849  cosknegpi  40080  fourierdlem58  40381  fourierdlem59  40382  fourierdlem72  40395  fourierdlem80  40403  sqwvfourb  40446  etransclem28  40479  etransclem41  40492  omef  40710  dfaimafn  41245  sbgoldbo  41675