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

Theorem 3eqtr4a 2341
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 2331 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2318 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623
This theorem is referenced by:  uniintsn  3899  iununi  3986  unizlim  4509  ordunisuc  4623  dmxpid  4898  rnxpid  5109  dmsnsnsn  5151  opswap  5159  fvco4i  5597  fndmdifcom  5630  offres  6092  1stval2  6137  2ndval2  6138  cnvf1olem  6216  fparlem3  6220  fparlem4  6221  seqomlem1  6462  ecovcom  6769  ecovass  6770  ecovdi  6771  resixpfo  6854  mapunen  7030  cardidm  7592  cardiun  7615  alephcard  7697  cardalephex  7717  cardcf  7878  cfidm  7901  alephsing  7902  itunisuc  8045  itunitc  8047  ituniiun  8048  alephadd  8199  alephreg  8204  pwcfsdom  8205  addcompq  8574  addcomnq  8575  mulcompq  8576  mulcomnq  8577  addassnq  8582  mulassnq  8583  addid1  8992  zeo  10097  xnegneg  10541  xaddcom  10565  xaddid1  10566  xnegdi  10568  xmulid1  10599  xadddilem  10614  ixxin  10673  fzsuc2  10842  expneg  11111  sq01  11223  facp1  11293  bcpasc  11333  hashf1lem1  11393  hashf1  11395  eqs1  11447  absexp  11789  sqreulem  11843  fsumf1o  12196  fsumadd  12211  fsumrev2  12244  fsumparts  12264  fsumrelem  12265  efexp  12381  tanval2  12413  sqr2irrlem  12526  sadeq  12663  smumullem  12683  smumul  12684  gcdcom  12699  gcd0id  12702  gcdass  12724  nn0gcdsq  12823  dfphi2  12842  pcneg  12926  setscom  13176  strfvi  13186  setsnid  13188  ressbas  13198  ressinbas  13204  ressress  13205  firest  13337  topnval  13339  xpsfeq  13466  xpsaddlem  13477  xpsvsca  13481  homffval  13594  oppchomfval  13617  cofuass  13763  setccatid  13916  xpcbas  13952  xpchomfval  13953  xpccofval  13956  oduleval  14235  oduglb  14243  odulub  14245  ipotset  14260  grpinvfvi  14523  symgbas  14772  symggrp  14780  cntrval  14795  cntzval  14797  oppgplusfval  14821  sylow1lem2  14910  sylow3lem1  14938  oppglsm  14953  gsumzsplit  15206  gsum2d  15223  gsumcom2  15226  dprd2dlem2  15275  dprd2da  15277  dmdprdsplit2lem  15280  mgpplusg  15329  mgpress  15336  rngidval  15343  opprmulfval  15407  abvtrivd  15605  sralem  15930  srasca  15934  sravsca  15935  rlmval  15945  psrmulr  16129  mplmonmul  16208  mplcoe3  16210  opsrbaslem  16219  opsrtoslem2  16226  psr1val  16265  ply1basfvi  16319  ply1plusgfvi  16320  psr1sca2  16329  zlmlem  16471  zlmsca  16475  zlmvsca  16476  ocvval  16567  thlbas  16596  thlle  16597  thloc  16599  tgdif0  16730  indislem  16737  restco  16895  txtopon  17286  txindislem  17327  qtopres  17389  hmphindis  17488  ptuncnv  17498  snclseqg  17798  tsmssplit  17834  setsmsbas  18021  tnglem  18156  tngds  18164  tngtset  18165  pcoass  18522  cphsqrcl2  18622  ovolunlem1a  18855  ioorinv  18931  itg11  19046  itg1mulc  19059  itg2cnlem1  19116  iblss2  19160  ibladdlem  19174  itgfsum  19181  iblabslem  19182  iblabs  19183  ditgneg  19207  deg1fvi  19471  dgrco  19656  logfac  19954  cxpexp  20015  cxpmul2  20036  cxpsqr  20050  dvcxp2  20083  ang180lem1  20107  mcubic  20143  quart1  20152  reasinsin  20192  atanlogaddlem  20209  atantayl2  20234  log2tlbnd  20241  basellem2  20319  basellem3  20320  basellem5  20322  basellem8  20325  dchrmulid2  20491  bcp1ctr  20518  lgsneg  20558  lgsneg1  20559  lgsdir2  20567  lgsdir  20569  lgsdi  20571  lgsquad2lem2  20598  pntleml  20760  bafval  21160  ipidsq  21286  ipasslem1  21409  pjclem2  22776  cvmdi  22904  iundisjcnt  23367  subfacp1lem6  23716  eupath2lem3  23903  dfrdg2  24152  dfrdg3  24153  dfrdg4  24488  ordtoplem  24874  ordcmp  24886  fsumprd  25329  hmeogrpi  25536  1ded  25738  idsubfun  25858  kelac2  27163  dsmmval2  27202  m1expaddsub  27421  mendbas  27492  mendsca  27497  mendrng  27500  iotain  27617  addrcom  27680  dpfrac1  28242  pmodN  30039  tgrpgrplem  30938  tendoplass  30972  tendoicl  30985  erngdvlem3  31179  dvhvaddass  31287  dib0  31354  dib1dim2  31358  diclspsn  31384  cdlemn8  31394  dihopelvalcpre  31438  djhcom  31595
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator