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

Theorem 3eqtr4a 2462
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 2452 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2439 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  uniintsn  4047  iununi  4135  unizlim  4657  ordunisuc  4771  dmxpid  5048  rnxpid  5261  dmsnsnsn  5307  opswap  5315  xpcoid  5374  fvco4i  5760  fndmdifcom  5794  offres  6278  1stval2  6323  2ndval2  6324  cnvf1olem  6403  fparlem3  6407  fparlem4  6408  seqomlem1  6666  ecovcom  6974  ecovass  6975  ecovdi  6976  resixpfo  7059  mapunen  7235  cardidm  7802  cardiun  7825  alephcard  7907  cardalephex  7927  cardcf  8088  cfidm  8111  alephsing  8112  itunisuc  8255  itunitc  8257  ituniiun  8258  alephadd  8408  alephreg  8413  pwcfsdom  8414  addcompq  8783  addcomnq  8784  mulcompq  8785  mulcomnq  8786  addassnq  8791  mulassnq  8792  addid1  9202  zeo  10311  xnegneg  10756  xaddcom  10780  xaddid1  10781  xnegdi  10783  xmulid1  10814  xadddilem  10829  ixxin  10889  fzsuc2  11060  expneg  11344  sq01  11456  facp1  11526  bcpasc  11567  hashf1lem1  11659  hashf1  11661  eqs1  11716  absexp  12064  sqreulem  12118  fsumf1o  12472  fsumadd  12487  fsumrev2  12520  fsumparts  12540  fsumrelem  12541  efexp  12657  tanval2  12689  sqr2irrlem  12802  sadeq  12939  smumullem  12959  smumul  12960  gcdcom  12975  gcd0id  12978  gcdass  13000  nn0gcdsq  13099  dfphi2  13118  pcneg  13202  setscom  13452  strfvi  13462  setsnid  13464  ressbas  13474  ressinbas  13480  ressress  13481  firest  13615  topnval  13617  xpsfeq  13744  xpsaddlem  13755  xpsvsca  13759  homffval  13872  oppchomfval  13895  oppcbas  13899  rescbas  13984  rescco  13987  cofuass  14041  fucbas  14112  fuchom  14113  setccatid  14194  xpcbas  14230  xpchomfval  14231  xpccofval  14234  oduleval  14513  oduglb  14521  odulub  14523  ipotset  14538  grpinvfvi  14801  symgbas  15050  symggrp  15058  cntrval  15073  cntzval  15075  oppgplusfval  15099  sylow1lem2  15188  sylow3lem1  15216  oppglsm  15231  gsumzsplit  15484  gsum2d  15501  gsumcom2  15504  dprd2dlem2  15553  dprd2da  15555  dmdprdsplit2lem  15558  mgpplusg  15607  mgpress  15614  rngidval  15621  opprmulfval  15685  abvtrivd  15883  sralem  16204  srasca  16208  sravsca  16209  rlmval  16219  psrmulr  16403  mplmonmul  16482  mplcoe3  16484  opsrbaslem  16493  opsrtoslem2  16500  psr1val  16539  ply1basfvi  16590  ply1plusgfvi  16591  psr1sca2  16600  zlmlem  16753  zlmsca  16757  zlmvsca  16758  ocvval  16849  thlbas  16878  thlle  16879  thloc  16881  tgdif0  17012  indislem  17019  restco  17182  txtopon  17576  txindislem  17618  qtopres  17683  hmphindis  17782  ptuncnv  17792  snclseqg  18098  tsmssplit  18134  ussval  18242  tuslem  18250  setsmsbas  18458  tnglem  18634  tngds  18642  tngtset  18643  pcoass  19002  cphsqrcl2  19102  ovolunlem1a  19345  ioorinv  19421  itg11  19536  itg1mulc  19549  itg2cnlem1  19606  iblss2  19650  ibladdlem  19664  itgfsum  19671  iblabslem  19672  iblabs  19673  ditgneg  19697  deg1fvi  19961  dgrco  20146  logfac  20448  cxpexp  20512  cxpmul2  20533  cxpsqr  20547  dvcxp2  20580  ang180lem1  20604  mcubic  20640  quart1  20649  reasinsin  20689  atanlogaddlem  20706  atantayl2  20731  log2tlbnd  20738  basellem2  20817  basellem3  20818  basellem5  20820  basellem8  20823  dchrmulid2  20989  bcp1ctr  21016  lgsneg  21056  lgsneg1  21057  lgsdir2  21065  lgsdir  21067  lgsdi  21069  lgsquad2lem2  21096  pntleml  21258  eupath2lem3  21654  bafval  22036  ipidsq  22162  ipasslem1  22285  pjclem2  23652  cvmdi  23780  imadifxp  23991  iundisjcnt  24107  indval2  24365  sitgclcn  24611  sitgclre  24612  bayesth  24650  subfacp1lem6  24824  fprodf1o  25225  fprodmul  25237  fproddiv  25238  fprodfac  25249  fallfacfwd  25303  dfrdg2  25366  dfrdg3  25367  dfrdg4  25703  ordtoplem  26089  ordcmp  26101  mblfinlem  26143  itg2addnclem2  26156  ibladdnclem  26160  iblabsnclem  26167  iblabsnc  26168  iblmulc2nc  26169  kelac2  27031  dsmmval2  27070  m1expaddsub  27289  mendbas  27360  mendsca  27365  mendrng  27368  iotain  27485  addrcom  27547  itgsinexplem1  27615  swrdccatin1  28016  swrdccat3b  28031  dpfrac1  28229  pmodN  30332  tgrpgrplem  31231  tendoplass  31265  tendoicl  31278  erngdvlem3  31472  dvhvaddass  31580  dib0  31647  dib1dim2  31651  diclspsn  31677  cdlemn8  31687  dihopelvalcpre  31731  djhcom  31888
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 2385
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2397
  Copyright terms: Public domain W3C validator