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

Theorem syl6reqr 2658
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 2614 . 2 𝐵 = 𝐶
41, 3syl6req 2656 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1711  ax-4 1726  ax-ext 2585
This theorem depends on definitions:  df-bi 195  df-cleq 2598
This theorem is referenced by:  iftrue  4037  iffalse  4040  difprsn1  4266  dmmptg  5531  setlikespec  5600  funimacnv  5866  dmmptd  5919  resasplit  5968  dffv3  6080  dfimafn  6136  fniinfv  6148  dffv2  6162  fvco2  6164  fniunfv  6383  isoini  6462  zfrep6  7000  oprabco  7121  oeeulem  7541  ixpconstg  7776  sbthlem4  7931  sbthlem5  7932  sbthlem6  7933  supval2  8217  hartogslem1  8303  cantnflem1d  8441  alephsuc2  8759  dfac3  8800  xp2cda  8858  hsmexlem5  9108  axdc2lem  9126  gruima  9476  eqneg  10590  zeo  11291  fseq1p1m1  12234  hashfzo  13024  hashimarn  13033  wrdval  13105  wrdnval  13132  repswswrd  13324  s1co  13372  swrds2  13475  modfsummod  14309  telfsumo  14317  mulgcd  15045  algcvg  15069  phiprmpw  15261  phisum  15275  strfv3  15678  resslem  15702  pwssnf1o  15923  imassca  15944  xpsfrn2  15995  homfeq  16119  oppcbas  16143  resscatc  16520  estrcbasbas  16536  funcestrcsetclem7  16551  funcestrcsetclem8  16552  funcestrcsetclem9  16553  fthestrcsetc  16555  fullestrcsetc  16556  equivestrcsetc  16557  setc1strwun  16558  funcsetcestrclem7  16566  funcsetcestrclem8  16567  funcsetcestrclem9  16568  fthsetcestrc  16570  fullsetcestrc  16571  lubsn  16859  ipotset  16922  ipole  16923  plusfeq  17014  pws0g  17091  frmd0  17162  oppgplusfval  17543  symgtset  17584  gsmsymgrfix  17613  gsmsymgreq  17617  psgnunilem2  17680  sylow3lem2  17808  oppglsm  17822  frgpuplem  17950  frgpupf  17951  frgpup1  17953  frgpup3lem  17955  gsumzoppg  18109  ablfac1eu  18237  pwsmgp  18383  opprmulfval  18390  dfrhm2  18482  subrg1  18555  staffn  18614  issrngd  18626  scafeq  18648  lbsextlem4  18924  sralem  18940  sravsca  18945  sraip  18946  rnascl  19106  psrlinv  19160  opsrbaslem  19240  opsrbaslemOLD  19241  evlseu  19279  mpfsubrg  19295  ply1scl0  19423  evl1sca  19461  evls1var  19465  zlmlem  19625  zlmvsca  19630  znbaslem  19646  znbaslemOLD  19647  ipfeq  19755  thlbas  19797  thlle  19798  thloc  19800  dsmmbase  19836  dsmmelbas  19840  frlmelbas  19857  frlmphl  19877  islindf4  19934  matbas  19976  matplusg  19977  matsca  19978  matvsca  19979  matbas2d  19986  matsubgcell  19997  matmulcell  20008  ofco2  20014  mattposm  20022  mat1f1o  20041  mdetunilem8  20182  madugsum  20206  cramerimplem2  20247  decpmatmullem  20333  paste  20846  ptpjcn  21162  uptx  21176  xpstopnlem1  21360  alexsubALTlem4  21602  cnextf  21618  submtmd  21656  ussval  21811  tuslem  21819  psmetge0  21865  xmetge0  21896  setsmsds  22028  tnglem  22188  tngtset  22197  tngngp2  22200  resubmet  22341  pcorev2  22563  om1plusg  22569  om1tset  22570  om1opn  22571  pi1grplem  22584  clmadd  22609  clmmul  22610  clmcj  22611  tchtopn  22750  tchnmfval  22752  bcthlem1  22842  bcthlem2  22843  bcthlem4  22845  bcth3  22849  rrxmval  22909  rrxmfval  22910  ehlbase  22915  minveclem3b  22920  pjthlem1  22929  volun  23033  voliun  23042  uniioovol  23066  itg2i1fseq  23241  itgcnlem  23275  iblabslem  23313  limcres  23369  cnplimc  23370  ply1termlem  23676  0dgr  23718  taylthlem1  23844  abelth  23912  lawcos  24259  lgambdd  24476  basellem8  24527  musum  24630  chtub  24650  dchrval  24672  dchrinvcl  24691  lgsval4lem  24746  lgsquadlem2  24819  m1lgs  24826  mirauto  25293  lmiisolem  25402  ttglem  25470  axlowdimlem16  25551  ebtwntg  25576  ecgrtg  25577  2pthlem2  25888  extwwlkfablem2  26367  smcnlem  26733  siii  26894  pjhthlem1  27436  sbcies  28508  imadifxp  28598  dfimafnf  28619  funcnvmptOLD  28652  funcnvmpt  28653  rdivmuldivd  28924  resvlem  28964  mdetpmtr12  29021  pstmval  29068  xpinpreima2  29083  pnfneige0  29127  zlmds  29138  zlmtset  29139  esumid  29235  esumrnmpt  29243  sxsigon  29384  carsgclctunlem1  29508  filnetlem4  31348  finxpreclem4  32206  itg2addnclem  32430  iblabsnclem  32442  areacirc  32474  fnopabco  32486  heiborlem8  32586  rngoi  32667  drngoi  32719  ldualvsub  33259  dalemrotyz  33761  dalem6  33771  dalem7  33772  dalem11  33777  dalem12  33778  dalemrotps  33794  dalem30  33805  dalem35  33810  cdleme1  34331  cdleme9  34357  cdleme20c  34416  cdleme20d  34417  cdlemefrs29clN  34504  cdleme37m  34567  cdleme43aN  34594  cdlemg1b2  34676  cdlemg4f  34720  cdlemh2  34921  erngdvlem1  35093  erngdvlem2N  35094  erngdvlem3  35095  erngdvlem4  35096  erngdvlem1-rN  35101  erngdvlem2-rN  35102  erngdvlem3-rN  35103  erngdvlem4-rN  35104  dvh4dimN  35553  lcdvsub  35723  hlhilsca  36044  hlhilbase  36045  hlhilplus  36046  hlhilvsca  36056  hlhilip  36057  hlhilipval  36058  mzpcompact2lem  36131  eldioph2lem1  36140  fiphp3d  36200  rmxypairf1o  36293  wopprc  36414  lmhmlnmsplit  36474  clcnvlem  36748  dmmptdf  38211  ellimcabssub0  38484  cosknegpi  38552  fourierdlem58  38857  fourierdlem59  38858  fourierdlem72  38871  fourierdlem80  38879  sqwvfourb  38922  etransclem28  38955  etransclem41  38968  dfaimafn  39695  funsneqopsn  40145  uspgrf1oedg  40401  nbgrval  40558  uvtxupgrres  40633  1wlkiswwlks2lem4  41067  1wlkiswwlks2lem5  41068  eucrct2eupth  41411
  Copyright terms: Public domain W3C validator