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

Theorem syl6reqr 2347
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 2300 . 2  |-  B  =  C
41, 3syl6req 2345 1  |-  ( ph  ->  C  =  A )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  iftrue  3584  iffalse  3585  difprsn1  3770  dmmptg  5186  relcoi1  5217  funimacnv  5340  resasplit  5427  dffv3  5537  dfimafn  5587  fniinfv  5597  dffv2  5608  fvco2  5610  zfrep6  5764  fniunfv  5789  isoini  5851  oprabco  6219  riotav  6325  oeeulem  6615  ixpconstg  6841  sbthlem4  6990  sbthlem5  6991  sbthlem6  6992  supval2  7222  hartogslem1  7273  cantnflem1d  7406  alephsuc2  7723  dfac3  7764  xp2cda  7822  hsmexlem5  8072  axdc2lem  8090  gruima  8440  eqneg  9496  zeo  10113  fseq1p1m1  10873  hashfzo  11399  wrdval  11432  s1co  11504  swrds2  11576  fsumtscopo  12276  mulgcd  12741  algcvg  12762  phiprmpw  12860  strfv3  13197  resslem  13217  pwssnf1o  13413  imassca  13438  xpsfrn2  13488  homfeq  13613  oppcbas  13637  resscatc  13953  lubsn  14216  ipotset  14276  ipole  14277  plusfeq  14397  pws0g  14424  frmd0  14498  symgtset  14795  oppgplusfval  14837  sylow3lem2  14955  oppglsm  14969  frgpuplem  15097  frgpupf  15098  frgpup1  15100  frgpup3lem  15102  gsumval3a  15205  gsumzoppg  15232  ablfac1eu  15324  pwsmgp  15417  opprmulfval  15423  dfrhm2  15514  subrg1  15571  staffn  15630  issrngd  15642  scafeq  15663  lbsextlem4  15930  sralem  15946  sravsca  15951  rnascl  16098  psrlinv  16158  opsrbaslem  16235  ply1scl0  16381  zlmlem  16487  zlmvsca  16492  znbaslem  16508  ipfeq  16570  thlbas  16612  thlle  16613  thloc  16615  paste  17038  ptpjcn  17321  uptx  17335  xpstopnlem1  17516  alexsubALTlem4  17760  submtmd  17803  xmetge0  17925  setsmsds  18038  tnglem  18172  tngtset  18181  tngngp2  18184  resubmet  18324  pcorev2  18542  om1plusg  18548  om1tset  18549  om1opn  18550  pi1grplem  18563  clmadd  18588  clmmul  18589  clmcj  18590  tchtopn  18673  tchnmfval  18675  bcthlem1  18762  bcthlem2  18763  bcthlem4  18765  bcth3  18769  minveclem3b  18808  pjthlem1  18817  volun  18918  voliun  18927  uniioovol  18950  itg2i1fseq  19126  itgcnlem  19160  iblabslem  19198  limcres  19252  cnplimc  19253  evlseu  19416  evl1sca  19429  mpfsubrg  19440  ply1termlem  19601  0dgr  19643  taylthlem1  19768  abelth  19833  lawcos  20130  basellem8  20341  musum  20447  chtub  20467  dchrval  20489  dchrinvcl  20508  lgsval4lem  20562  lgsquadlem2  20610  m1lgs  20617  rngoi  21063  drngoi  21090  smcnlem  21286  siii  21447  pjhthlem1  21986  dfimafnf  23057  funcnvmptOLD  23249  funcnvmpt  23250  xpinpreima2  23306  esumid  23439  sxsigon  23538  setlikespec  24258  axlowdimlem16  24657  iblabsnclem  25014  areacirc  25034  cbcpcp  25265  fnopabco2b  25474  ltrcmp  25508  rngounval2  25528  limhun  25673  limptlimpr2lem1  25677  supexr  25734  filnetlem4  26433  fnopabco  26491  heiborlem8  26645  mzpcompact2lem  26932  eldioph2lem1  26942  fiphp3d  27005  rmxypairf1o  27099  wopprc  27226  lmhmlnmsplit  27288  dsmmbase  27304  dsmmelbas  27308  frlmelbas  27327  islindf4  27411  psgnunilem2  27521  matbas  27571  matplusg  27572  matsca  27573  matvsca  27574  phisum  27621  dfaimafn  28133  ldualvsub  29967  dalemrotyz  30469  dalem6  30479  dalem7  30480  dalem11  30485  dalem12  30486  dalemrotps  30502  dalem30  30513  dalem35  30518  cdleme1  31038  cdleme9  31064  cdleme20c  31122  cdleme20d  31123  cdlemefrs29clN  31210  cdleme37m  31273  cdleme43aN  31300  cdlemg1b2  31382  cdlemg4f  31426  cdlemh2  31627  erngdvlem1  31799  erngdvlem2N  31800  erngdvlem3  31801  erngdvlem4  31802  erngdvlem1-rN  31807  erngdvlem2-rN  31808  erngdvlem3-rN  31809  erngdvlem4-rN  31810  dvh4dimN  32259  lcdvsub  32429  hlhilsca  32750  hlhilbase  32751  hlhilplus  32752  hlhilvsca  32762  hlhilip  32763  hlhilipval  32764
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator