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

Theorem syl6reqr 2818
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 2774 . 2 𝐵 = 𝐶
41, 3syl6req 2816 1 (𝜑𝐶 = 𝐴)
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1652
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1890  ax-4 1904  ax-5 2005  ax-6 2070  ax-7 2105  ax-9 2164  ax-ext 2743
This theorem depends on definitions:  df-bi 198  df-an 385  df-ex 1875  df-cleq 2758
This theorem is referenced by:  iftrue  4249  iffalse  4252  difprsn1  4485  dmmptg  5818  setlikespec  5886  funimacnv  6148  dmmptd  6202  resasplit  6256  dffv3  6371  dfimafn  6434  fniinfv  6446  dffv2  6460  fvco2  6462  funsneqopsnOLD  6609  fniunfv  6697  isoini  6780  zfrep6  7332  oprabco  7463  oeeulem  7886  ixpconstg  8122  sbthlem4  8280  sbthlem5  8281  sbthlem6  8282  supval2  8568  hartogslem1  8654  cantnflem1d  8800  alephsuc2  9154  dfac3  9195  xp2cda  9255  hsmexlem5  9505  axdc2lem  9523  gruima  9877  eqneg  10999  zeo  11710  fseq1p1m1  12621  hashfzo  13417  hashimarn  13428  wrdval  13489  wrdnval  13516  repswswrd  13808  s1co  13862  swrds2  13969  modfsummod  14810  telfsumo  14818  mulgcd  15546  algcvg  15570  phiprmpw  15760  phisum  15774  strfv3  16180  resslem  16205  pwssnf1o  16424  imassca  16445  xpsfrn2  16496  homfeq  16619  oppcbas  16643  resscatc  17020  estrcbasbas  17036  funcestrcsetclem7  17052  funcestrcsetclem8  17053  funcestrcsetclem9  17054  fthestrcsetc  17056  fullestrcsetc  17057  equivestrcsetc  17058  setc1strwun  17059  funcsetcestrclem7  17067  funcsetcestrclem8  17068  funcsetcestrclem9  17069  fthsetcestrc  17071  fullsetcestrc  17072  lubsn  17360  ipotset  17423  ipole  17424  plusfeq  17515  pws0g  17592  frmd0  17664  oppgplusfval  18041  symgtset  18082  gsmsymgrfix  18111  gsmsymgreq  18115  psgnunilem2  18179  sylow3lem2  18307  oppglsm  18321  frgpuplem  18451  frgpupf  18452  frgpup1  18454  frgpup3lem  18456  gsumzoppg  18610  ablfac1eu  18739  pwsmgp  18885  opprmulfval  18892  dfrhm2  18986  subrg1  19059  staffn  19118  issrngd  19130  scafeq  19152  lbsextlem4  19435  sralem  19451  sravsca  19456  sraip  19457  rnascl  19617  psrlinv  19671  opsrbaslem  19751  evlseu  19789  mpfsubrg  19805  ply1scl0  19933  evl1sca  19971  evls1var  19975  zlmlem  20138  zlmvsca  20143  znbaslem  20159  ipfeq  20270  ssipeq  20276  thlbas  20316  thlle  20317  thloc  20319  dsmmbase  20355  dsmmelbas  20359  frlmelbas  20376  frlmphl  20396  islindf4  20453  matbas  20495  matplusg  20496  matsca  20497  matvsca  20498  matbas2d  20505  matsubgcell  20516  matmulcell  20527  matmulcellOLD  20528  ofco2  20534  mattposm  20542  mat1f1o  20561  mdetunilem8  20702  madugsum  20726  cramerimplem2  20769  decpmatmullem  20855  paste  21378  ptpjcn  21694  uptx  21708  xpstopnlem1  21892  alexsubALTlem4  22133  cnextf  22149  submtmd  22187  ussval  22342  tuslem  22350  psmetge0  22396  xmetge0  22428  setsmsds  22560  sgrim  22714  tnglem  22723  tngtset  22732  tngngp2  22735  resubmet  22884  pcorev2  23106  om1plusg  23112  om1tset  23113  om1opn  23114  pi1grplem  23127  clmadd  23152  clmmul  23153  clmcj  23154  tcphtopn  23303  tchnmfval  23305  bcthlem1  23401  bcthlem2  23402  bcthlem4  23404  bcth3  23408  rrxmval  23477  rrxmfval  23478  ehlbase  23483  minveclem3b  23488  pjthlem1  23497  volun  23603  voliun  23612  uniioovol  23637  itg2i1fseq  23813  itgcnlem  23847  iblabslem  23885  limcres  23941  cnplimc  23942  ply1termlem  24250  0dgr  24292  taylthlem1  24418  abelth  24486  lawcos  24837  lgambdd  25054  basellem8  25105  musum  25208  chtub  25228  dchrval  25250  dchrinvcl  25269  lgsval4lem  25324  lgsquadlem2  25397  m1lgs  25404  mirauto  25870  lmiisolem  25979  ttglem  26047  axlowdimlem16  26128  ebtwntg  26153  ecgrtg  26154  nbgrval  26508  uvtxupgrres  26594  clwlknf1oclwwlknlem3  27349  clwlknf1oclwwlknlem3OLD  27351  eucrct2eupth  27523  smcnlem  28008  siii  28164  pjhthlem1  28706  sbcies  29778  imadifxp  29862  dfimafnf  29886  funcnvmpt  29917  rdivmuldivd  30238  resvlem  30278  mdetpmtr12  30338  pstmval  30385  xpinpreima2  30400  pnfneige0  30444  zlmds  30455  zlmtset  30456  esumid  30553  esumrnmpt  30561  sxsigon  30702  carsgclctunlem1  30826  circlemethnat  31170  filnetlem4  32819  setsstrset  33517  finxpreclem4  33664  itg2addnclem  33884  iblabsnclem  33896  areacirc  33928  fnopabco  33940  heiborlem8  34039  rngoi  34120  drngoi  34172  ldualvsub  35111  dalemrotyz  35614  dalem6  35624  dalem7  35625  dalem11  35630  dalem12  35631  dalemrotps  35647  dalem30  35658  dalem35  35663  cdleme1  36183  cdleme9  36209  cdleme20c  36267  cdleme20d  36268  cdlemefrs29clN  36355  cdleme37m  36418  cdleme43aN  36445  cdlemg1b2  36527  cdlemg4f  36571  cdlemh2  36772  erngdvlem1  36944  erngdvlem2N  36945  erngdvlem3  36946  erngdvlem4  36947  erngdvlem1-rN  36952  erngdvlem2-rN  36953  erngdvlem3-rN  36954  erngdvlem4-rN  36955  dvh4dimN  37403  lcdvsub  37573  hlhilsca  37891  hlhilbase  37892  hlhilplus  37893  hlhilvsca  37903  hlhilip  37904  hlhilipval  37905  mzpcompact2lem  37992  eldioph2lem1  38001  fiphp3d  38061  rmxypairf1o  38153  wopprc  38274  lmhmlnmsplit  38334  clcnvlem  38605  dmmptdf  40062  dmmptdf2  40081  ellimcabssub0  40487  cosknegpi  40718  fourierdlem58  41018  fourierdlem59  41019  fourierdlem72  41032  fourierdlem80  41040  sqwvfourb  41083  etransclem28  41116  etransclem41  41129  omef  41350  dfaimafn  41913  afv2co2  42005  sbgoldbo  42351
  Copyright terms: Public domain W3C validator