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

Theorem 3eqtr4a 2354
Description: A chained equality inference, useful for converting to definitions. (Contributed by NM, 2-Feb-2007.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4a.1  |-  A  =  B
3eqtr4a.2  |-  ( ph  ->  C  =  A )
3eqtr4a.3  |-  ( ph  ->  D  =  B )
Assertion
Ref Expression
3eqtr4a  |-  ( ph  ->  C  =  D )

Proof of Theorem 3eqtr4a
StepHypRef Expression
1 3eqtr4a.2 . . 3  |-  ( ph  ->  C  =  A )
2 3eqtr4a.1 . . 3  |-  A  =  B
31, 2syl6eq 2344 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2331 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632
This theorem is referenced by:  uniintsn  3915  iununi  4002  unizlim  4525  ordunisuc  4639  dmxpid  4914  rnxpid  5125  dmsnsnsn  5167  opswap  5175  fvco4i  5613  fndmdifcom  5646  offres  6108  1stval2  6153  2ndval2  6154  cnvf1olem  6232  fparlem3  6236  fparlem4  6237  seqomlem1  6478  ecovcom  6785  ecovass  6786  ecovdi  6787  resixpfo  6870  mapunen  7046  cardidm  7608  cardiun  7631  alephcard  7713  cardalephex  7733  cardcf  7894  cfidm  7917  alephsing  7918  itunisuc  8061  itunitc  8063  ituniiun  8064  alephadd  8215  alephreg  8220  pwcfsdom  8221  addcompq  8590  addcomnq  8591  mulcompq  8592  mulcomnq  8593  addassnq  8598  mulassnq  8599  addid1  9008  zeo  10113  xnegneg  10557  xaddcom  10581  xaddid1  10582  xnegdi  10584  xmulid1  10615  xadddilem  10630  ixxin  10689  fzsuc2  10858  expneg  11127  sq01  11239  facp1  11309  bcpasc  11349  hashf1lem1  11409  hashf1  11411  eqs1  11463  absexp  11805  sqreulem  11859  fsumf1o  12212  fsumadd  12227  fsumrev2  12260  fsumparts  12280  fsumrelem  12281  efexp  12397  tanval2  12429  sqr2irrlem  12542  sadeq  12679  smumullem  12699  smumul  12700  gcdcom  12715  gcd0id  12718  gcdass  12740  nn0gcdsq  12839  dfphi2  12858  pcneg  12942  setscom  13192  strfvi  13202  setsnid  13204  ressbas  13214  ressinbas  13220  ressress  13221  firest  13353  topnval  13355  xpsfeq  13482  xpsaddlem  13493  xpsvsca  13497  homffval  13610  oppchomfval  13633  cofuass  13779  setccatid  13932  xpcbas  13968  xpchomfval  13969  xpccofval  13972  oduleval  14251  oduglb  14259  odulub  14261  ipotset  14276  grpinvfvi  14539  symgbas  14788  symggrp  14796  cntrval  14811  cntzval  14813  oppgplusfval  14837  sylow1lem2  14926  sylow3lem1  14954  oppglsm  14969  gsumzsplit  15222  gsum2d  15239  gsumcom2  15242  dprd2dlem2  15291  dprd2da  15293  dmdprdsplit2lem  15296  mgpplusg  15345  mgpress  15352  rngidval  15359  opprmulfval  15423  abvtrivd  15621  sralem  15946  srasca  15950  sravsca  15951  rlmval  15961  psrmulr  16145  mplmonmul  16224  mplcoe3  16226  opsrbaslem  16235  opsrtoslem2  16242  psr1val  16281  ply1basfvi  16335  ply1plusgfvi  16336  psr1sca2  16345  zlmlem  16487  zlmsca  16491  zlmvsca  16492  ocvval  16583  thlbas  16612  thlle  16613  thloc  16615  tgdif0  16746  indislem  16753  restco  16911  txtopon  17302  txindislem  17343  qtopres  17405  hmphindis  17504  ptuncnv  17514  snclseqg  17814  tsmssplit  17850  setsmsbas  18037  tnglem  18172  tngds  18180  tngtset  18181  pcoass  18538  cphsqrcl2  18638  ovolunlem1a  18871  ioorinv  18947  itg11  19062  itg1mulc  19075  itg2cnlem1  19132  iblss2  19176  ibladdlem  19190  itgfsum  19197  iblabslem  19198  iblabs  19199  ditgneg  19223  deg1fvi  19487  dgrco  19672  logfac  19970  cxpexp  20031  cxpmul2  20052  cxpsqr  20066  dvcxp2  20099  ang180lem1  20123  mcubic  20159  quart1  20168  reasinsin  20208  atanlogaddlem  20225  atantayl2  20250  log2tlbnd  20257  basellem2  20335  basellem3  20336  basellem5  20338  basellem8  20341  dchrmulid2  20507  bcp1ctr  20534  lgsneg  20574  lgsneg1  20575  lgsdir2  20583  lgsdir  20585  lgsdi  20587  lgsquad2lem2  20614  pntleml  20776  bafval  21176  ipidsq  21302  ipasslem1  21425  pjclem2  22792  cvmdi  22920  iundisjcnt  23382  subfacp1lem6  23731  eupath2lem3  23918  fprodf1o  24172  dfrdg2  24223  dfrdg3  24224  dfrdg4  24560  ordtoplem  24946  ordcmp  24958  itg2addnclem2  25004  ibladdnclem  25007  iblabsnclem  25014  iblabsnc  25015  iblmulc2nc  25016  fsumprd  25432  hmeogrpi  25639  1ded  25841  idsubfun  25961  kelac2  27266  dsmmval2  27305  m1expaddsub  27524  mendbas  27595  mendsca  27600  mendrng  27603  iotain  27720  addrcom  27783  dpfrac1  28496  pmodN  30661  tgrpgrplem  31560  tendoplass  31594  tendoicl  31607  erngdvlem3  31801  dvhvaddass  31909  dib0  31976  dib1dim2  31980  diclspsn  32006  cdlemn8  32016  dihopelvalcpre  32060  djhcom  32217
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