Theorem syl6reqr 2881

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 2835	. 2 ⊢ 𝐵 = 𝐶
4	1, 3	syl6req 2879	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1658

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-ext 2804

This theorem depends on definitions:  df-bi 199  df-an 387  df-ex 1881  df-cleq 2819

This theorem is referenced by:  iftrue  4313  iffalse  4316  difprsn1  4550  dmmptg  5874  setlikespec  5942  funimacnv  6204  dmmptd  6258  resasplit  6312  dffv3  6430  dfimafn  6493  fniinfv  6505  dffv2  6519  fvco2  6521  funsneqopsnOLD  6669  fniunfv  6761  isoini  6844  zfrep6  7397  oprabco  7526  oeeulem  7949  ixpconstg  8185  sbthlem4  8343  sbthlem5  8344  sbthlem6  8345  supval2  8631  hartogslem1  8717  cantnflem1d  8863  alephsuc2  9217  dfac3  9258  xp2cda  9318  hsmexlem5  9568  axdc2lem  9586  gruima  9940  eqneg  11072  zeo  11792  fseq1p1m1  12709  hashfzo  13506  hashimarn  13517  wrdval  13578  wrdnval  13606  repswswrd  13901  s1co  13955  swrds2  14062  modfsummod  14901  telfsumo  14909  mulgcd  15639  algcvg  15663  phiprmpw  15853  phisum  15867  strfv3  16272  resslem  16297  pwssnf1o  16512  imassca  16533  xpsfrn2  16584  homfeq  16707  oppcbas  16731  resscatc  17108  estrcbasbas  17124  funcestrcsetclem7  17140  funcestrcsetclem8  17141  funcestrcsetclem9  17142  fthestrcsetc  17144  fullestrcsetc  17145  equivestrcsetc  17146  setc1strwun  17147  funcsetcestrclem7  17155  funcsetcestrclem8  17156  funcsetcestrclem9  17157  fthsetcestrc  17159  fullsetcestrc  17160  lubsn  17448  ipotset  17511  ipole  17512  plusfeq  17603  pws0g  17680  frmd0  17752  oppgplusfval  18129  symgtset  18170  gsmsymgrfix  18199  gsmsymgreq  18203  psgnunilem2  18267  sylow3lem2  18395  oppglsm  18409  frgpuplem  18539  frgpupf  18540  frgpup1  18542  frgpup3lem  18544  gsumzoppg  18698  ablfac1eu  18827  pwsmgp  18973  opprmulfval  18980  dfrhm2  19074  subrg1  19147  staffn  19206  issrngd  19218  scafeq  19240  lbsextlem4  19523  sralem  19539  sravsca  19544  sraip  19545  rnascl  19705  psrlinv  19759  opsrbaslem  19839  evlseu  19877  mpfsubrg  19893  ply1scl0  20021  evl1sca  20059  evls1var  20063  zlmlem  20226  zlmvsca  20231  znbaslem  20247  ipfeq  20358  ssipeq  20364  thlbas  20404  thlle  20405  thloc  20407  dsmmbase  20443  dsmmelbas  20447  frlmelbas  20464  frlmphl  20488  islindf4  20545  matbas  20587  matplusg  20588  matsca  20589  matvsca  20590  matbas2d  20597  matsubgcell  20608  matmulcell  20619  matmulcellOLD  20620  ofco2  20626  mattposm  20634  mat1f1o  20653  mdetunilem8  20794  madugsum  20818  cramerimplem2  20861  decpmatmullem  20947  paste  21470  ptpjcn  21786  uptx  21800  xpstopnlem1  21984  alexsubALTlem4  22225  cnextf  22241  submtmd  22279  ussval  22434  tuslem  22442  psmetge0  22488  xmetge0  22520  setsmsds  22652  sgrim  22806  tnglem  22815  tngtset  22824  tngngp2  22827  resubmet  22976  pcorev2  23198  om1plusg  23204  om1tset  23205  om1opn  23206  pi1grplem  23219  clmadd  23244  clmmul  23245  clmcj  23246  tcphtopn  23395  tchnmfval  23397  bcthlem1  23493  bcthlem2  23494  bcthlem4  23496  bcth3  23500  rrxmval  23574  rrxmfval  23575  ehlbase  23584  minveclem3b  23597  pjthlem1  23606  volun  23712  voliun  23721  uniioovol  23746  itg2i1fseq  23922  itgcnlem  23956  iblabslem  23994  limcres  24050  cnplimc  24051  ply1termlem  24359  0dgr  24401  taylthlem1  24527  abelth  24595  lawcos  24957  lgambdd  25177  basellem8  25228  musum  25331  chtub  25351  dchrval  25373  dchrinvcl  25392  lgsval4lem  25447  lgsquadlem2  25520  m1lgs  25527  mirauto  25997  lmiisolem  26106  ttglem  26176  axlowdimlem16  26257  ebtwntg  26282  ecgrtg  26283  elntg2  26285  nbgrval  26634  uvtxupgrres  26707  clwlknf1oclwwlknlem3  27451  clwlknf1oclwwlknlem3OLD  27453  eucrct2eupthOLD  27624  eucrct2eupth  27625  smcnlem  28108  siii  28264  pjhthlem1  28806  sbcies  29878  imadifxp  29962  dfimafnf  29986  funcnvmpt  30017  rdivmuldivd  30337  resvlem  30377  mdetpmtr12  30437  pstmval  30484  xpinpreima2  30499  pnfneige0  30543  zlmds  30554  zlmtset  30555  esumid  30652  esumrnmpt  30660  sxsigon  30801  carsgclctunlem1  30925  circlemethnat  31269  filnetlem4  32915  setsstrset  33613  finxpreclem4  33777  itg2addnclem  34005  iblabsnclem  34017  areacirc  34049  fnopabco  34061  heiborlem8  34160  rngoi  34241  drngoi  34293  ldualvsub  35231  dalemrotyz  35734  dalem6  35744  dalem7  35745  dalem11  35750  dalem12  35751  dalemrotps  35767  dalem30  35778  dalem35  35783  cdleme1  36303  cdleme9  36329  cdleme20c  36387  cdleme20d  36388  cdlemefrs29clN  36475  cdleme37m  36538  cdleme43aN  36565  cdlemg1b2  36647  cdlemg4f  36691  cdlemh2  36892  erngdvlem1  37064  erngdvlem2N  37065  erngdvlem3  37066  erngdvlem4  37067  erngdvlem1-rN  37072  erngdvlem2-rN  37073  erngdvlem3-rN  37074  erngdvlem4-rN  37075  dvh4dimN  37523  lcdvsub  37693  hlhilsca  38011  hlhilbase  38012  hlhilplus  38013  hlhilvsca  38023  hlhilip  38024  hlhilipval  38025  mzpcompact2lem  38159  eldioph2lem1  38168  fiphp3d  38228  rmxypairf1o  38320  wopprc  38441  lmhmlnmsplit  38501  clcnvlem  38772  dmmptdf  40224  dmmptdf2  40242  ellimcabssub0  40645  cosknegpi  40876  fourierdlem58  41176  fourierdlem59  41177  fourierdlem72  41190  fourierdlem80  41198  sqwvfourb  41241  etransclem28  41274  etransclem41  41287  omef  41505  dfaimafn  42068  afv2co2  42160  sbgoldbo  42506  rrxlinesc  43287  rrxlinec  43288  rrxsphere  43301  itsclinecirc0  43315