MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  syl6reqr Structured version   Visualization version   GIF version

Theorem syl6reqr 2673
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
StepHypRef Expression
1 syl6reqr.1 . 2 (𝜑𝐴 = 𝐵)
2 syl6reqr.2 . . 3 𝐶 = 𝐵
32eqcomi 2629 . 2 𝐵 = 𝐶
41, 3syl6req 2671 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1481
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-an 386  df-ex 1703  df-cleq 2613
This theorem is referenced by:  iftrue  4083  iffalse  4086  difprsn1  4321  dmmptg  5620  setlikespec  5689  funimacnv  5958  dmmptd  6011  resasplit  6061  dffv3  6174  dfimafn  6232  fniinfv  6244  dffv2  6258  fvco2  6260  funsneqopsn  6402  fniunfv  6490  isoini  6573  zfrep6  7119  oprabco  7246  oeeulem  7666  ixpconstg  7902  sbthlem4  8058  sbthlem5  8059  sbthlem6  8060  supval2  8346  hartogslem1  8432  cantnflem1d  8570  alephsuc2  8888  dfac3  8929  xp2cda  8987  hsmexlem5  9237  axdc2lem  9255  gruima  9609  eqneg  10730  zeo  11448  fseq1p1m1  12398  hashfzo  13199  hashimarn  13210  wrdval  13291  wrdnval  13318  repswswrd  13512  s1co  13560  swrds2  13666  modfsummod  14507  telfsumo  14515  mulgcd  15246  algcvg  15270  phiprmpw  15462  phisum  15476  strfv3  15889  resslem  15914  pwssnf1o  16139  imassca  16160  xpsfrn2  16211  homfeq  16335  oppcbas  16359  resscatc  16736  estrcbasbas  16752  funcestrcsetclem7  16767  funcestrcsetclem8  16768  funcestrcsetclem9  16769  fthestrcsetc  16771  fullestrcsetc  16772  equivestrcsetc  16773  setc1strwun  16774  funcsetcestrclem7  16782  funcsetcestrclem8  16783  funcsetcestrclem9  16784  fthsetcestrc  16786  fullsetcestrc  16787  lubsn  17075  ipotset  17138  ipole  17139  plusfeq  17230  pws0g  17307  frmd0  17378  oppgplusfval  17759  symgtset  17800  gsmsymgrfix  17829  gsmsymgreq  17833  psgnunilem2  17896  sylow3lem2  18024  oppglsm  18038  frgpuplem  18166  frgpupf  18167  frgpup1  18169  frgpup3lem  18171  gsumzoppg  18325  ablfac1eu  18453  pwsmgp  18599  opprmulfval  18606  dfrhm2  18698  subrg1  18771  staffn  18830  issrngd  18842  scafeq  18864  lbsextlem4  19142  sralem  19158  sravsca  19163  sraip  19164  rnascl  19324  psrlinv  19378  opsrbaslem  19458  opsrbaslemOLD  19459  evlseu  19497  mpfsubrg  19513  ply1scl0  19641  evl1sca  19679  evls1var  19683  zlmlem  19846  zlmvsca  19851  znbaslem  19867  znbaslemOLD  19868  ipfeq  19976  ssipeq  19982  thlbas  20021  thlle  20022  thloc  20024  dsmmbase  20060  dsmmelbas  20064  frlmelbas  20081  frlmphl  20101  islindf4  20158  matbas  20200  matplusg  20201  matsca  20202  matvsca  20203  matbas2d  20210  matsubgcell  20221  matmulcell  20232  ofco2  20238  mattposm  20246  mat1f1o  20265  mdetunilem8  20406  madugsum  20430  cramerimplem2  20471  decpmatmullem  20557  paste  21079  ptpjcn  21395  uptx  21409  xpstopnlem1  21593  alexsubALTlem4  21835  cnextf  21851  submtmd  21889  ussval  22044  tuslem  22052  psmetge0  22098  xmetge0  22130  setsmsds  22262  sgrim  22416  tnglem  22425  tngtset  22434  tngngp2  22437  resubmet  22586  pcorev2  22809  om1plusg  22815  om1tset  22816  om1opn  22817  pi1grplem  22830  clmadd  22855  clmmul  22856  clmcj  22857  tchtopn  23006  tchnmfval  23008  bcthlem1  23102  bcthlem2  23103  bcthlem4  23105  bcth3  23109  rrxmval  23169  rrxmfval  23170  ehlbase  23175  minveclem3b  23180  pjthlem1  23189  volun  23294  voliun  23303  uniioovol  23328  itg2i1fseq  23503  itgcnlem  23537  iblabslem  23575  limcres  23631  cnplimc  23632  ply1termlem  23940  0dgr  23982  taylthlem1  24108  abelth  24176  lawcos  24527  lgambdd  24744  basellem8  24795  musum  24898  chtub  24918  dchrval  24940  dchrinvcl  24959  lgsval4lem  25014  lgsquadlem2  25087  m1lgs  25094  mirauto  25560  lmiisolem  25669  ttglem  25737  axlowdimlem16  25818  ebtwntg  25843  ecgrtg  25844  nbgrval  26215  uvtxupgrres  26290  eucrct2eupth  27085  smcnlem  27522  siii  27678  pjhthlem1  28220  sbcies  29294  imadifxp  29386  dfimafnf  29409  funcnvmptOLD  29441  funcnvmpt  29442  rdivmuldivd  29765  resvlem  29805  mdetpmtr12  29865  pstmval  29912  xpinpreima2  29927  pnfneige0  29971  zlmds  29982  zlmtset  29983  esumid  30080  esumrnmpt  30088  sxsigon  30229  carsgclctunlem1  30353  circlemethnat  30693  filnetlem4  32351  finxpreclem4  33202  itg2addnclem  33432  iblabsnclem  33444  areacirc  33476  fnopabco  33488  heiborlem8  33588  rngoi  33669  drngoi  33721  ldualvsub  34261  dalemrotyz  34763  dalem6  34773  dalem7  34774  dalem11  34779  dalem12  34780  dalemrotps  34796  dalem30  34807  dalem35  34812  cdleme1  35333  cdleme9  35359  cdleme20c  35418  cdleme20d  35419  cdlemefrs29clN  35506  cdleme37m  35569  cdleme43aN  35596  cdlemg1b2  35678  cdlemg4f  35722  cdlemh2  35923  erngdvlem1  36095  erngdvlem2N  36096  erngdvlem3  36097  erngdvlem4  36098  erngdvlem1-rN  36103  erngdvlem2-rN  36104  erngdvlem3-rN  36105  erngdvlem4-rN  36106  dvh4dimN  36555  lcdvsub  36725  hlhilsca  37046  hlhilbase  37047  hlhilplus  37048  hlhilvsca  37058  hlhilip  37059  hlhilipval  37060  mzpcompact2lem  37133  eldioph2lem1  37142  fiphp3d  37202  rmxypairf1o  37295  wopprc  37416  lmhmlnmsplit  37476  clcnvlem  37749  dmmptdf  39233  dmmptdf2  39255  ellimcabssub0  39649  cosknegpi  39843  fourierdlem58  40144  fourierdlem59  40145  fourierdlem72  40158  fourierdlem80  40166  sqwvfourb  40209  etransclem28  40242  etransclem41  40255  omef  40473  dfaimafn  41008  sbgoldbo  41440
  Copyright terms: Public domain W3C validator