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

Theorem 3eqtr4a 2510
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 2500 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2487 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1383
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-cleq 2435
This theorem is referenced by:  rabsnif  4084  uniintsn  4309  iinvdif  4387  iununi  4400  unizlim  4984  dmxpid  5212  rnxpid  5430  csbrn  5458  dmsnsnsn  5476  opswap  5485  xpcoid  5538  fvco4i  5936  fndmdifcom  5977  fmptsng  6077  fmptsnd  6078  csbov  6316  ordunisuc  6652  offres  6780  1stval2  6802  2ndval2  6803  cnvf1olem  6883  fparlem3  6887  fparlem4  6888  imacosupp  6942  seqomlem1  7117  ecovcom  7419  ecovass  7420  ecovdi  7421  resixpfo  7509  mapunen  7688  cardidm  8343  cardiun  8366  alephcard  8454  cardalephex  8474  cardcf  8635  cfidm  8658  alephsing  8659  itunisuc  8802  itunitc  8804  ituniiun  8805  alephadd  8955  alephreg  8960  pwcfsdom  8961  addcompq  9331  addcomnq  9332  mulcompq  9333  mulcomnq  9334  addassnq  9339  mulassnq  9340  addid1  9763  zeo  10954  xnegneg  11422  xaddcom  11446  xaddid1  11447  xnegdi  11449  xmulid1  11480  xadddilem  11495  ixxin  11555  fzsuc2  11746  expneg  12153  sq01  12267  facp1  12337  bcpasc  12378  hashf1lem1  12483  hashf1  12485  eqs1  12600  swrdccatin1  12687  swrdccat3blem  12699  repswsymballbi  12731  cshwmodn  12745  repswcshw  12759  absexp  13116  sqreulem  13171  fsumf1o  13524  fsumadd  13540  fsumrev2  13576  fsumparts  13599  fsumrelem  13600  efexp  13713  tanval2  13745  sqr2irrlem  13858  sadeq  13999  smumullem  14019  smumul  14020  gcdcom  14035  gcd0id  14038  gcdass  14060  nn0gcdsq  14162  dfphi2  14181  pcneg  14274  setscom  14539  strfvi  14549  setsnid  14551  ressbas  14564  ressinbas  14570  ressress  14571  firest  14707  topnval  14709  xpsfeq  14838  xpsaddlem  14849  xpsvsca  14853  homffval  14963  oppchomfval  14986  oppcbas  14990  rescbas  15075  rescco  15078  cofuass  15132  fucbas  15203  fuchom  15204  setccatid  15285  xpcbas  15321  xpchomfval  15322  xpccofval  15325  oduleval  15635  oduglb  15643  odulub  15645  ipotset  15661  grpinvfvi  15965  cntrval  16231  cntzval  16233  oppgplusfval  16257  symgbas  16279  symggrp  16299  pmtrprfval  16386  m1expaddsub  16397  sylow1lem2  16493  sylow3lem1  16521  oppglsm  16536  gsumzsplit  16818  gsumzsplitOLD  16819  gsum2dlem2  16872  gsum2dOLD  16874  gsumcom2  16877  dprd2dlem2  16963  dprd2da  16965  dmdprdsplit2lem  16968  mgpplusg  17019  mgpress  17026  ringidval  17029  opprmulfval  17148  abvtrivd  17363  sralem  17697  srasca  17701  sravsca  17702  sraip  17703  rlmval  17711  psrmulr  17911  mplmonmul  18000  mplcoe3  18002  mplcoe3OLD  18003  opsrbaslem  18016  opsrtoslem2  18023  psr1val  18099  ply1basfvi  18156  ply1plusgfvi  18157  psr1sca2  18166  evl1fval1lem  18240  zlmlem  18427  zlmsca  18431  zlmvsca  18432  psgninv  18491  ocvval  18571  thlbas  18600  thlle  18601  thloc  18603  dsmmval2  18640  mattpos1  18831  mdettpos  18986  smadiadetglem1  19046  tgdif0  19367  indislem  19374  restco  19538  txtopon  19965  txindislem  20007  qtopres  20072  hmphindis  20171  ptuncnv  20181  snclseqg  20487  tsmssplit  20527  ussval  20635  tuslem  20643  setsmsbas  20851  tnglem  21027  tngds  21035  tngtset  21036  pcoass  21397  cphsqrtcl2  21506  rrxcph  21697  ovolunlem1a  21780  ioorinv  21858  itg11  21971  itg1mulc  21984  itg2cnlem1  22041  iblss2  22085  ibladdlem  22099  itgfsum  22106  iblabslem  22107  iblabs  22108  ditgneg  22134  deg1fvi  22358  dgrco  22544  logfac  22857  cxpexp  22921  cxpmul2  22942  cxpsqrt  22956  dvcxp1  22988  dvcxp2  22989  ang180lem1  23013  mcubic  23050  quart1  23059  reasinsin  23099  atanlogaddlem  23116  atantayl2  23141  log2tlbnd  23148  basellem2  23227  basellem3  23228  basellem5  23230  basellem8  23233  dchrmulid2  23399  bcp1ctr  23426  lgsneg  23466  lgsneg1  23467  lgsdir2  23475  lgsdir  23477  lgsdi  23479  lgsquad2lem2  23506  pntleml  23668  motgrp  23802  lmiisolem  24033  ttglem  24051  eupath2lem3  24851  bafval  25369  ipidsq  25495  ipasslem1  25618  pjclem2  26987  cvmdi  27115  imadifxp  27330  iundisjcnt  27475  resvsca  27693  indval2  27901  bayesth  28251  plymulx  28378  subfacp1lem6  28502  mvtval  28733  mexval  28735  mexval2  28736  mdvval  28737  mrsubfval  28741  mrsubvrs  28755  msubfval  28757  elmsubrn  28761  mvhfval  28766  mpstval  28768  msrfval  28770  mstaval  28777  mthmval  28808  fprodf1o  29053  fprodmul  29065  fproddiv  29066  fprodfac  29077  fallfacfwd  29133  dfrdg2  29203  dfrdg3  29204  dfrdg4  29575  ordtoplem  29875  ordcmp  29887  mblfinlem2  30027  itg2addnclem2  30042  ibladdnclem  30046  iblabsnclem  30053  iblabsnc  30054  iblmulc2nc  30055  ftc1anclem8  30072  kelac2  30986  mendbas  31109  mendsca  31114  mendring  31117  lcmcom  31175  lcmneg  31185  lcmass  31194  iotain  31278  addrcom  31338  itgsinexplem1  31642  volioc  31661  dirkertrigeqlem1  31769  fourierdlem104  31882  sqwvfoura  31900  sqwvfourb  31901  estrccatid  32484  rngccatidOLD  32534  ringccatidOLD  32592  dpfrac1  32896  pmodN  35308  tgrpgrplem  36209  tendoplass  36243  tendoicl  36256  erngdvlem3  36450  dvhvaddass  36558  dib0  36625  dib1dim2  36629  diclspsn  36655  cdlemn8  36665  dihopelvalcpre  36709  djhcom  36866
  Copyright terms: Public domain W3C validator