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

Theorem syl6reqr 2494
Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)
Hypotheses
Ref Expression
syl6reqr.1  |-  ( ph  ->  A  =  B )
syl6reqr.2  |-  C  =  B
Assertion
Ref Expression
syl6reqr  |-  ( ph  ->  C  =  A )

Proof of Theorem syl6reqr
StepHypRef Expression
1 syl6reqr.1 . 2  |-  ( ph  ->  A  =  B )
2 syl6reqr.2 . . 3  |-  C  =  B
32eqcomi 2447 . 2  |-  B  =  C
41, 3syl6req 2492 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1369
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-ex 1587  df-cleq 2436
This theorem is referenced by:  iftrue  3802  iffalse  3804  difprsn1  4015  dmmptg  5340  relcoi1  5371  funimacnv  5495  resasplit  5586  dffv3  5692  dfimafn  5745  fniinfv  5755  dffv2  5769  fvco2  5771  fniunfv  5969  isoini  6034  zfrep6  6550  oprabco  6662  oeeulem  7045  ixpconstg  7277  sbthlem4  7429  sbthlem5  7430  sbthlem6  7431  supval2  7710  hartogslem1  7761  cantnflem1d  7901  cantnflem1dOLD  7924  alephsuc2  8255  dfac3  8296  xp2cda  8354  hsmexlem5  8604  axdc2lem  8622  gruima  8974  eqneg  10056  zeo  10732  fseq1p1m1  11539  hashfzo  12195  hashimarn  12205  wrdval  12243  repswswrd  12427  s1co  12466  swrds2  12550  fsumtscopo  13270  mulgcd  13735  algcvg  13756  phiprmpw  13856  strfv3  14214  resslem  14236  pwssnf1o  14441  imassca  14462  xpsfrn2  14513  homfeq  14638  oppcbas  14662  resscatc  14978  lubsn  15269  ipotset  15332  ipole  15333  plusfeq  15434  pws0g  15462  frmd0  15543  oppgplusfval  15868  symgtset  15909  gsmsymgrfix  15938  gsmsymgreq  15942  psgnunilem2  16006  sylow3lem2  16132  oppglsm  16146  frgpuplem  16274  frgpupf  16275  frgpup1  16277  frgpup3lem  16279  gsumval3aOLD  16385  gsumzoppg  16445  gsumzoppgOLD  16446  ablfac1eu  16579  pwsmgp  16715  opprmulfval  16722  dfrhm2  16813  subrg1  16880  staffn  16939  issrngd  16951  scafeq  16973  lbsextlem4  17247  sralem  17263  sravsca  17268  sraip  17269  rnascl  17418  psrlinv  17473  opsrbaslem  17564  evlseu  17607  mpfsubrg  17623  ply1scl0  17747  evl1sca  17773  evls1var  17777  zlmlem  17953  zlmvsca  17958  znbaslem  17976  ipfeq  18084  thlbas  18126  thlle  18127  thloc  18129  dsmmbase  18165  dsmmelbas  18169  frlmelbas  18187  frlmelbasOLD  18188  frlmphl  18211  islindf4  18272  matbas  18319  matplusg  18320  matsca  18321  matvsca  18322  matbas2d  18329  ofco2  18337  mattposm  18349  mdetunilem8  18430  madugsum  18454  cramerimplem2  18495  paste  18903  ptpjcn  19189  uptx  19203  xpstopnlem1  19387  alexsubALTlem4  19627  cnextf  19643  submtmd  19680  ussval  19839  tuslem  19847  psmetge0  19893  xmetge0  19924  setsmsds  20056  tnglem  20231  tngtset  20240  tngngp2  20243  resubmet  20384  pcorev2  20605  om1plusg  20611  om1tset  20612  om1opn  20613  pi1grplem  20626  clmadd  20651  clmmul  20652  clmcj  20653  tchtopn  20746  tchnmfval  20748  bcthlem1  20840  bcthlem2  20841  bcthlem4  20843  bcth3  20847  rrxmval  20909  rrxmfval  20910  ehlbase  20915  minveclem3b  20920  pjthlem1  20929  volun  21031  voliun  21040  uniioovol  21064  itg2i1fseq  21238  itgcnlem  21272  iblabslem  21310  limcres  21366  cnplimc  21367  ply1termlem  21676  0dgr  21718  taylthlem1  21843  abelth  21911  lawcos  22217  basellem8  22430  musum  22536  chtub  22556  dchrval  22578  dchrinvcl  22597  lgsval4lem  22651  lgsquadlem2  22699  m1lgs  22706  mirauto  23083  ttglem  23127  axlowdimlem16  23208  ebtwntg  23233  ecgrtg  23234  2pthlem2  23500  rngoi  23872  drngoi  23899  smcnlem  24097  siii  24258  pjhthlem1  24799  sbcies  25871  imadifxp  25944  dfimafnf  25955  funcnvmptOLD  25991  funcnvmpt  25992  rdivmuldivd  26264  resvlem  26304  pstmval  26327  xpinpreima2  26342  pnfneige0  26386  zlmds  26398  zlmtset  26399  esumid  26504  sxsigon  26611  lgambdd  27028  setlikespec  27653  itg2addnclem  28448  iblabsnclem  28460  areacirc  28494  filnetlem4  28607  fnopabco  28621  heiborlem8  28722  mzpcompact2lem  29093  eldioph2lem1  29103  fiphp3d  29163  rmxypairf1o  29257  wopprc  29384  lmhmlnmsplit  29445  phisum  29572  dfaimafn  30076  modfsummod  30250  wrdnval  30479  extwwlkfablem2  30676  matsubgcell  30865  pmatcollpw1dstlem1  30905  ldualvsub  32805  dalemrotyz  33307  dalem6  33317  dalem7  33318  dalem11  33323  dalem12  33324  dalemrotps  33340  dalem30  33351  dalem35  33356  cdleme1  33876  cdleme9  33902  cdleme20c  33960  cdleme20d  33961  cdlemefrs29clN  34048  cdleme37m  34111  cdleme43aN  34138  cdlemg1b2  34220  cdlemg4f  34264  cdlemh2  34465  erngdvlem1  34637  erngdvlem2N  34638  erngdvlem3  34639  erngdvlem4  34640  erngdvlem1-rN  34645  erngdvlem2-rN  34646  erngdvlem3-rN  34647  erngdvlem4-rN  34648  dvh4dimN  35097  lcdvsub  35267  hlhilsca  35588  hlhilbase  35589  hlhilplus  35590  hlhilvsca  35600  hlhilip  35601  hlhilipval  35602
  Copyright terms: Public domain W3C validator