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

Theorem 3eqtr4a 2470
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 2460 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2447 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  uniintsn  4055  iununi  4143  unizlim  4665  ordunisuc  4779  dmxpid  5056  rnxpid  5269  dmsnsnsn  5315  opswap  5323  xpcoid  5382  fvco4i  5768  fndmdifcom  5802  offres  6286  1stval2  6331  2ndval2  6332  cnvf1olem  6411  fparlem3  6415  fparlem4  6416  seqomlem1  6674  ecovcom  6982  ecovass  6983  ecovdi  6984  resixpfo  7067  mapunen  7243  cardidm  7810  cardiun  7833  alephcard  7915  cardalephex  7935  cardcf  8096  cfidm  8119  alephsing  8120  itunisuc  8263  itunitc  8265  ituniiun  8266  alephadd  8416  alephreg  8421  pwcfsdom  8422  addcompq  8791  addcomnq  8792  mulcompq  8793  mulcomnq  8794  addassnq  8799  mulassnq  8800  addid1  9210  zeo  10319  xnegneg  10764  xaddcom  10788  xaddid1  10789  xnegdi  10791  xmulid1  10822  xadddilem  10837  ixxin  10897  fzsuc2  11068  expneg  11352  sq01  11464  facp1  11534  bcpasc  11575  hashf1lem1  11667  hashf1  11669  eqs1  11724  absexp  12072  sqreulem  12126  fsumf1o  12480  fsumadd  12495  fsumrev2  12528  fsumparts  12548  fsumrelem  12549  efexp  12665  tanval2  12697  sqr2irrlem  12810  sadeq  12947  smumullem  12967  smumul  12968  gcdcom  12983  gcd0id  12986  gcdass  13008  nn0gcdsq  13107  dfphi2  13126  pcneg  13210  setscom  13460  strfvi  13470  setsnid  13472  ressbas  13482  ressinbas  13488  ressress  13489  firest  13623  topnval  13625  xpsfeq  13752  xpsaddlem  13763  xpsvsca  13767  homffval  13880  oppchomfval  13903  oppcbas  13907  rescbas  13992  rescco  13995  cofuass  14049  fucbas  14120  fuchom  14121  setccatid  14202  xpcbas  14238  xpchomfval  14239  xpccofval  14242  oduleval  14521  oduglb  14529  odulub  14531  ipotset  14546  grpinvfvi  14809  symgbas  15058  symggrp  15066  cntrval  15081  cntzval  15083  oppgplusfval  15107  sylow1lem2  15196  sylow3lem1  15224  oppglsm  15239  gsumzsplit  15492  gsum2d  15509  gsumcom2  15512  dprd2dlem2  15561  dprd2da  15563  dmdprdsplit2lem  15566  mgpplusg  15615  mgpress  15622  rngidval  15629  opprmulfval  15693  abvtrivd  15891  sralem  16212  srasca  16216  sravsca  16217  rlmval  16227  psrmulr  16411  mplmonmul  16490  mplcoe3  16492  opsrbaslem  16501  opsrtoslem2  16508  psr1val  16547  ply1basfvi  16598  ply1plusgfvi  16599  psr1sca2  16608  zlmlem  16761  zlmsca  16765  zlmvsca  16766  ocvval  16857  thlbas  16886  thlle  16887  thloc  16889  tgdif0  17020  indislem  17027  restco  17190  txtopon  17584  txindislem  17626  qtopres  17691  hmphindis  17790  ptuncnv  17800  snclseqg  18106  tsmssplit  18142  ussval  18250  tuslem  18258  setsmsbas  18466  tnglem  18642  tngds  18650  tngtset  18651  pcoass  19010  cphsqrcl2  19110  ovolunlem1a  19353  ioorinv  19429  itg11  19544  itg1mulc  19557  itg2cnlem1  19614  iblss2  19658  ibladdlem  19672  itgfsum  19679  iblabslem  19680  iblabs  19681  ditgneg  19705  deg1fvi  19969  dgrco  20154  logfac  20456  cxpexp  20520  cxpmul2  20541  cxpsqr  20555  dvcxp2  20588  ang180lem1  20612  mcubic  20648  quart1  20657  reasinsin  20697  atanlogaddlem  20714  atantayl2  20739  log2tlbnd  20746  basellem2  20825  basellem3  20826  basellem5  20828  basellem8  20831  dchrmulid2  20997  bcp1ctr  21024  lgsneg  21064  lgsneg1  21065  lgsdir2  21073  lgsdir  21075  lgsdi  21077  lgsquad2lem2  21104  pntleml  21266  eupath2lem3  21662  bafval  22044  ipidsq  22170  ipasslem1  22293  pjclem2  23660  cvmdi  23788  imadifxp  23999  iundisjcnt  24115  indval2  24373  sitgclcn  24619  sitgclre  24620  bayesth  24658  subfacp1lem6  24832  fprodf1o  25233  fprodmul  25245  fproddiv  25246  fprodfac  25257  fallfacfwd  25311  dfrdg2  25374  dfrdg3  25375  dfrdg4  25711  ordtoplem  26097  ordcmp  26109  mblfinlem  26151  itg2addnclem2  26164  ibladdnclem  26168  iblabsnclem  26175  iblabsnc  26176  iblmulc2nc  26177  kelac2  27039  dsmmval2  27078  m1expaddsub  27297  mendbas  27368  mendsca  27373  mendrng  27376  iotain  27493  addrcom  27555  itgsinexplem1  27623  swrdccatin1  28024  swrdccat3b  28039  dpfrac1  28237  pmodN  30344  tgrpgrplem  31243  tendoplass  31277  tendoicl  31290  erngdvlem3  31484  dvhvaddass  31592  dib0  31659  dib1dim2  31663  diclspsn  31689  cdlemn8  31699  dihopelvalcpre  31743  djhcom  31900
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 2393
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2405
  Copyright terms: Public domain W3C validator