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

Theorem syl6reqr 2704
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 2660 . 2 𝐵 = 𝐶
41, 3syl6req 2702 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-an 385  df-ex 1745  df-cleq 2644
This theorem is referenced by:  iftrue  4125  iffalse  4128  difprsn1  4362  dmmptg  5670  setlikespec  5739  funimacnv  6008  dmmptd  6062  resasplit  6112  dffv3  6225  dfimafn  6284  fniinfv  6296  dffv2  6310  fvco2  6312  funsneqopsn  6457  fniunfv  6545  isoini  6628  zfrep6  7176  oprabco  7306  oeeulem  7726  ixpconstg  7959  sbthlem4  8114  sbthlem5  8115  sbthlem6  8116  supval2  8402  hartogslem1  8488  cantnflem1d  8623  alephsuc2  8941  dfac3  8982  xp2cda  9040  hsmexlem5  9290  axdc2lem  9308  gruima  9662  eqneg  10783  zeo  11501  fseq1p1m1  12452  hashfzo  13254  hashimarn  13265  wrdval  13340  wrdnval  13367  repswswrd  13577  s1co  13625  swrds2  13731  modfsummod  14570  telfsumo  14578  mulgcd  15312  algcvg  15336  phiprmpw  15528  phisum  15542  strfv3  15955  resslem  15980  pwssnf1o  16205  imassca  16226  xpsfrn2  16277  homfeq  16401  oppcbas  16425  resscatc  16802  estrcbasbas  16818  funcestrcsetclem7  16833  funcestrcsetclem8  16834  funcestrcsetclem9  16835  fthestrcsetc  16837  fullestrcsetc  16838  equivestrcsetc  16839  setc1strwun  16840  funcsetcestrclem7  16848  funcsetcestrclem8  16849  funcsetcestrclem9  16850  fthsetcestrc  16852  fullsetcestrc  16853  lubsn  17141  ipotset  17204  ipole  17205  plusfeq  17296  pws0g  17373  frmd0  17444  oppgplusfval  17824  symgtset  17865  gsmsymgrfix  17894  gsmsymgreq  17898  psgnunilem2  17961  sylow3lem2  18089  oppglsm  18103  frgpuplem  18231  frgpupf  18232  frgpup1  18234  frgpup3lem  18236  gsumzoppg  18390  ablfac1eu  18518  pwsmgp  18664  opprmulfval  18671  dfrhm2  18765  subrg1  18838  staffn  18897  issrngd  18909  scafeq  18931  lbsextlem4  19209  sralem  19225  sravsca  19230  sraip  19231  rnascl  19391  psrlinv  19445  opsrbaslem  19525  opsrbaslemOLD  19526  evlseu  19564  mpfsubrg  19580  ply1scl0  19708  evl1sca  19746  evls1var  19750  zlmlem  19913  zlmvsca  19918  znbaslem  19934  znbaslemOLD  19935  ipfeq  20043  ssipeq  20049  thlbas  20088  thlle  20089  thloc  20091  dsmmbase  20127  dsmmelbas  20131  frlmelbas  20148  frlmphl  20168  islindf4  20225  matbas  20267  matplusg  20268  matsca  20269  matvsca  20270  matbas2d  20277  matsubgcell  20288  matmulcell  20299  ofco2  20305  mattposm  20313  mat1f1o  20332  mdetunilem8  20473  madugsum  20497  cramerimplem2  20538  decpmatmullem  20624  paste  21146  ptpjcn  21462  uptx  21476  xpstopnlem1  21660  alexsubALTlem4  21901  cnextf  21917  submtmd  21955  ussval  22110  tuslem  22118  psmetge0  22164  xmetge0  22196  setsmsds  22328  sgrim  22482  tnglem  22491  tngtset  22500  tngngp2  22503  resubmet  22652  pcorev2  22874  om1plusg  22880  om1tset  22881  om1opn  22882  pi1grplem  22895  clmadd  22920  clmmul  22921  clmcj  22922  tchtopn  23071  tchnmfval  23073  bcthlem1  23167  bcthlem2  23168  bcthlem4  23170  bcth3  23174  rrxmval  23234  rrxmfval  23235  ehlbase  23240  minveclem3b  23245  pjthlem1  23254  volun  23359  voliun  23368  uniioovol  23393  itg2i1fseq  23567  itgcnlem  23601  iblabslem  23639  limcres  23695  cnplimc  23696  ply1termlem  24004  0dgr  24046  taylthlem1  24172  abelth  24240  lawcos  24591  lgambdd  24808  basellem8  24859  musum  24962  chtub  24982  dchrval  25004  dchrinvcl  25023  lgsval4lem  25078  lgsquadlem2  25151  m1lgs  25158  mirauto  25624  lmiisolem  25733  ttglem  25801  axlowdimlem16  25882  ebtwntg  25907  ecgrtg  25908  nbgrval  26274  uvtxupgrres  26359  eucrct2eupth  27223  smcnlem  27680  siii  27836  pjhthlem1  28378  sbcies  29450  imadifxp  29540  dfimafnf  29564  funcnvmptOLD  29595  funcnvmpt  29596  rdivmuldivd  29919  resvlem  29959  mdetpmtr12  30019  pstmval  30066  xpinpreima2  30081  pnfneige0  30125  zlmds  30136  zlmtset  30137  esumid  30234  esumrnmpt  30242  sxsigon  30383  carsgclctunlem1  30507  circlemethnat  30847  filnetlem4  32501  setsstrset  33214  finxpreclem4  33361  itg2addnclem  33591  iblabsnclem  33603  areacirc  33635  fnopabco  33647  heiborlem8  33747  rngoi  33828  drngoi  33880  ldualvsub  34760  dalemrotyz  35262  dalem6  35272  dalem7  35273  dalem11  35278  dalem12  35279  dalemrotps  35295  dalem30  35306  dalem35  35311  cdleme1  35832  cdleme9  35858  cdleme20c  35916  cdleme20d  35917  cdlemefrs29clN  36004  cdleme37m  36067  cdleme43aN  36094  cdlemg1b2  36176  cdlemg4f  36220  cdlemh2  36421  erngdvlem1  36593  erngdvlem2N  36594  erngdvlem3  36595  erngdvlem4  36596  erngdvlem1-rN  36601  erngdvlem2-rN  36602  erngdvlem3-rN  36603  erngdvlem4-rN  36604  dvh4dimN  37053  lcdvsub  37223  hlhilsca  37544  hlhilbase  37545  hlhilplus  37546  hlhilvsca  37556  hlhilip  37557  hlhilipval  37558  mzpcompact2lem  37631  eldioph2lem1  37640  fiphp3d  37700  rmxypairf1o  37793  wopprc  37914  lmhmlnmsplit  37974  clcnvlem  38247  dmmptdf  39731  dmmptdf2  39753  ellimcabssub0  40167  cosknegpi  40398  fourierdlem58  40699  fourierdlem59  40700  fourierdlem72  40713  fourierdlem80  40721  sqwvfourb  40764  etransclem28  40797  etransclem41  40810  omef  41031  dfaimafn  41566  sbgoldbo  42000
  Copyright terms: Public domain W3C validator