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

Theorem syl6reqr 2455
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 2408 . 2  |-  B  =  C
41, 3syl6req 2453 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  iftrue  3705  iffalse  3706  difprsn1  3895  dmmptg  5326  relcoi1  5357  funimacnv  5484  resasplit  5572  dffv3  5683  dfimafn  5734  fniinfv  5744  dffv2  5755  fvco2  5757  zfrep6  5927  fniunfv  5953  isoini  6017  oprabco  6390  riotav  6513  oeeulem  6803  ixpconstg  7030  sbthlem4  7179  sbthlem5  7180  sbthlem6  7181  supval2  7416  hartogslem1  7467  cantnflem1d  7600  alephsuc2  7917  dfac3  7958  xp2cda  8016  hsmexlem5  8266  axdc2lem  8284  gruima  8633  eqneg  9690  zeo  10311  fseq1p1m1  11077  hashfzo  11649  wrdval  11685  s1co  11757  swrds2  11835  fsumtscopo  12536  mulgcd  13001  algcvg  13022  phiprmpw  13120  strfv3  13457  resslem  13477  pwssnf1o  13675  imassca  13700  xpsfrn2  13750  homfeq  13875  oppcbas  13899  resscatc  14215  lubsn  14478  ipotset  14538  ipole  14539  plusfeq  14659  pws0g  14686  frmd0  14760  symgtset  15057  oppgplusfval  15099  sylow3lem2  15217  oppglsm  15231  frgpuplem  15359  frgpupf  15360  frgpup1  15362  frgpup3lem  15364  gsumval3a  15467  gsumzoppg  15494  ablfac1eu  15586  pwsmgp  15679  opprmulfval  15685  dfrhm2  15776  subrg1  15833  staffn  15892  issrngd  15904  scafeq  15925  lbsextlem4  16188  sralem  16204  sravsca  16209  rnascl  16356  psrlinv  16416  opsrbaslem  16493  ply1scl0  16636  zlmlem  16753  zlmvsca  16758  znbaslem  16774  ipfeq  16836  thlbas  16878  thlle  16879  thloc  16881  paste  17312  ptpjcn  17596  uptx  17610  xpstopnlem1  17794  alexsubALTlem4  18034  cnextf  18050  submtmd  18087  ussval  18242  tuslem  18250  psmetge0  18296  xmetge0  18327  setsmsds  18459  tnglem  18634  tngtset  18643  tngngp2  18646  resubmet  18786  pcorev2  19006  om1plusg  19012  om1tset  19013  om1opn  19014  pi1grplem  19027  clmadd  19052  clmmul  19053  clmcj  19054  tchtopn  19137  tchnmfval  19139  bcthlem1  19230  bcthlem2  19231  bcthlem4  19233  bcth3  19237  minveclem3b  19282  pjthlem1  19291  volun  19392  voliun  19401  uniioovol  19424  itg2i1fseq  19600  itgcnlem  19634  iblabslem  19672  limcres  19726  cnplimc  19727  evlseu  19890  evl1sca  19903  mpfsubrg  19914  ply1termlem  20075  0dgr  20117  taylthlem1  20242  abelth  20310  lawcos  20611  basellem8  20823  musum  20929  chtub  20949  dchrval  20971  dchrinvcl  20990  lgsval4lem  21044  lgsquadlem2  21092  m1lgs  21099  2pthlem2  21549  rngoi  21921  drngoi  21948  smcnlem  22146  siii  22307  pjhthlem1  22846  imadifxp  23991  dfimafnf  23996  funcnvmptOLD  24035  funcnvmpt  24036  rdivmuldivd  24180  pstmval  24243  xpinpreima2  24258  pnfneige0  24289  zlmds  24301  zlmtset  24302  esumid  24393  sxsigon  24499  lgambdd  24774  setlikespec  25401  axlowdimlem16  25800  itg2addnclem  26155  iblabsnclem  26167  areacirc  26187  filnetlem4  26300  fnopabco  26314  heiborlem8  26417  mzpcompact2lem  26698  eldioph2lem1  26708  fiphp3d  26770  rmxypairf1o  26864  wopprc  26991  lmhmlnmsplit  27053  dsmmbase  27069  dsmmelbas  27073  frlmelbas  27092  islindf4  27176  psgnunilem2  27286  matbas  27336  matplusg  27337  matsca  27338  matvsca  27339  phisum  27386  dfaimafn  27896  hashimarn  27994  ldualvsub  29638  dalemrotyz  30140  dalem6  30150  dalem7  30151  dalem11  30156  dalem12  30157  dalemrotps  30173  dalem30  30184  dalem35  30189  cdleme1  30709  cdleme9  30735  cdleme20c  30793  cdleme20d  30794  cdlemefrs29clN  30881  cdleme37m  30944  cdleme43aN  30971  cdlemg1b2  31053  cdlemg4f  31097  cdlemh2  31298  erngdvlem1  31470  erngdvlem2N  31471  erngdvlem3  31472  erngdvlem4  31473  erngdvlem1-rN  31478  erngdvlem2-rN  31479  erngdvlem3-rN  31480  erngdvlem4-rN  31481  dvh4dimN  31930  lcdvsub  32100  hlhilsca  32421  hlhilbase  32422  hlhilplus  32423  hlhilvsca  32433  hlhilip  32434  hlhilipval  32435
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-11 1757  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator