Theorem syl6reqr 2663

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
syl6reqr.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6reqr.2	⊢ 𝐶 = 𝐵

Assertion

Ref	Expression
syl6reqr	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem syl6reqr

Step	Hyp	Ref	Expression
1		syl6reqr.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6reqr.2	. . 3 ⊢ 𝐶 = 𝐵
3	2	eqcomi 2619	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6req 2661	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-cleq 2603

This theorem is referenced by:  iftrue  4042  iffalse  4045  difprsn1  4271  dmmptg  5549  setlikespec  5618  funimacnv  5884  dmmptd  5937  resasplit  5987  dffv3  6099  dfimafn  6155  fniinfv  6167  dffv2  6181  fvco2  6183  funsneqopsn  6322  fniunfv  6409  isoini  6488  zfrep6  7027  oprabco  7148  oeeulem  7568  ixpconstg  7803  sbthlem4  7958  sbthlem5  7959  sbthlem6  7960  supval2  8244  hartogslem1  8330  cantnflem1d  8468  alephsuc2  8786  dfac3  8827  xp2cda  8885  hsmexlem5  9135  axdc2lem  9153  gruima  9503  eqneg  10624  zeo  11339  fseq1p1m1  12283  hashfzo  13076  hashimarn  13085  wrdval  13163  wrdnval  13190  repswswrd  13382  s1co  13430  swrds2  13533  modfsummod  14367  telfsumo  14375  mulgcd  15103  algcvg  15127  phiprmpw  15319  phisum  15333  strfv3  15736  resslem  15760  pwssnf1o  15981  imassca  16002  xpsfrn2  16053  homfeq  16177  oppcbas  16201  resscatc  16578  estrcbasbas  16594  funcestrcsetclem7  16609  funcestrcsetclem8  16610  funcestrcsetclem9  16611  fthestrcsetc  16613  fullestrcsetc  16614  equivestrcsetc  16615  setc1strwun  16616  funcsetcestrclem7  16624  funcsetcestrclem8  16625  funcsetcestrclem9  16626  fthsetcestrc  16628  fullsetcestrc  16629  lubsn  16917  ipotset  16980  ipole  16981  plusfeq  17072  pws0g  17149  frmd0  17220  oppgplusfval  17601  symgtset  17642  gsmsymgrfix  17671  gsmsymgreq  17675  psgnunilem2  17738  sylow3lem2  17866  oppglsm  17880  frgpuplem  18008  frgpupf  18009  frgpup1  18011  frgpup3lem  18013  gsumzoppg  18167  ablfac1eu  18295  pwsmgp  18441  opprmulfval  18448  dfrhm2  18540  subrg1  18613  staffn  18672  issrngd  18684  scafeq  18706  lbsextlem4  18982  sralem  18998  sravsca  19003  sraip  19004  rnascl  19164  psrlinv  19218  opsrbaslem  19298  opsrbaslemOLD  19299  evlseu  19337  mpfsubrg  19353  ply1scl0  19481  evl1sca  19519  evls1var  19523  zlmlem  19684  zlmvsca  19689  znbaslem  19705  znbaslemOLD  19706  ipfeq  19814  ssipeq  19820  thlbas  19859  thlle  19860  thloc  19862  dsmmbase  19898  dsmmelbas  19902  frlmelbas  19919  frlmphl  19939  islindf4  19996  matbas  20038  matplusg  20039  matsca  20040  matvsca  20041  matbas2d  20048  matsubgcell  20059  matmulcell  20070  ofco2  20076  mattposm  20084  mat1f1o  20103  mdetunilem8  20244  madugsum  20268  cramerimplem2  20309  decpmatmullem  20395  paste  20908  ptpjcn  21224  uptx  21238  xpstopnlem1  21422  alexsubALTlem4  21664  cnextf  21680  submtmd  21718  ussval  21873  tuslem  21881  psmetge0  21927  xmetge0  21959  setsmsds  22091  sgrim  22245  tnglem  22254  tngtset  22263  tngngp2  22266  resubmet  22413  pcorev2  22636  om1plusg  22642  om1tset  22643  om1opn  22644  pi1grplem  22657  clmadd  22682  clmmul  22683  clmcj  22684  tchtopn  22833  tchnmfval  22835  bcthlem1  22929  bcthlem2  22930  bcthlem4  22932  bcth3  22936  rrxmval  22996  rrxmfval  22997  ehlbase  23002  minveclem3b  23007  pjthlem1  23016  volun  23120  voliun  23129  uniioovol  23153  itg2i1fseq  23328  itgcnlem  23362  iblabslem  23400  limcres  23456  cnplimc  23457  ply1termlem  23763  0dgr  23805  taylthlem1  23931  abelth  23999  lawcos  24346  lgambdd  24563  basellem8  24614  musum  24717  chtub  24737  dchrval  24759  dchrinvcl  24778  lgsval4lem  24833  lgsquadlem2  24906  m1lgs  24913  mirauto  25379  lmiisolem  25488  ttglem  25556  axlowdimlem16  25637  ebtwntg  25662  ecgrtg  25663  2pthlem2  26126  extwwlkfablem2  26605  smcnlem  26936  siii  27092  pjhthlem1  27634  sbcies  28706  imadifxp  28796  dfimafnf  28817  funcnvmptOLD  28850  funcnvmpt  28851  rdivmuldivd  29122  resvlem  29162  mdetpmtr12  29219  pstmval  29266  xpinpreima2  29281  pnfneige0  29325  zlmds  29336  zlmtset  29337  esumid  29433  esumrnmpt  29441  sxsigon  29582  carsgclctunlem1  29706  filnetlem4  31546  finxpreclem4  32407  itg2addnclem  32631  iblabsnclem  32643  areacirc  32675  fnopabco  32687  heiborlem8  32787  rngoi  32868  drngoi  32920  ldualvsub  33460  dalemrotyz  33962  dalem6  33972  dalem7  33973  dalem11  33978  dalem12  33979  dalemrotps  33995  dalem30  34006  dalem35  34011  cdleme1  34532  cdleme9  34558  cdleme20c  34617  cdleme20d  34618  cdlemefrs29clN  34705  cdleme37m  34768  cdleme43aN  34795  cdlemg1b2  34877  cdlemg4f  34921  cdlemh2  35122  erngdvlem1  35294  erngdvlem2N  35295  erngdvlem3  35296  erngdvlem4  35297  erngdvlem1-rN  35302  erngdvlem2-rN  35303  erngdvlem3-rN  35304  erngdvlem4-rN  35305  dvh4dimN  35754  lcdvsub  35924  hlhilsca  36245  hlhilbase  36246  hlhilplus  36247  hlhilvsca  36257  hlhilip  36258  hlhilipval  36259  mzpcompact2lem  36332  eldioph2lem1  36341  fiphp3d  36401  rmxypairf1o  36494  wopprc  36615  lmhmlnmsplit  36675  clcnvlem  36949  dmmptdf  38412  ellimcabssub0  38684  cosknegpi  38752  fourierdlem58  39057  fourierdlem59  39058  fourierdlem72  39071  fourierdlem80  39079  sqwvfourb  39122  etransclem28  39155  etransclem41  39168  dfaimafn  39894  uspgrf1oedg  40403  nbgrval  40560  uvtxupgrres  40635  1wlkiswwlks2lem4  41069  1wlkiswwlks2lem5  41070  eucrct2eupth  41413