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

Theorem 3eqtr4a 2438
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 2428 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2415 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1649
This theorem is referenced by:  uniintsn  4022  iununi  4109  unizlim  4631  ordunisuc  4745  dmxpid  5022  rnxpid  5235  dmsnsnsn  5281  opswap  5289  xpcoid  5348  fvco4i  5733  fndmdifcom  5767  offres  6251  1stval2  6296  2ndval2  6297  cnvf1olem  6376  fparlem3  6380  fparlem4  6381  seqomlem1  6636  ecovcom  6944  ecovass  6945  ecovdi  6946  resixpfo  7029  mapunen  7205  cardidm  7772  cardiun  7795  alephcard  7877  cardalephex  7897  cardcf  8058  cfidm  8081  alephsing  8082  itunisuc  8225  itunitc  8227  ituniiun  8228  alephadd  8378  alephreg  8383  pwcfsdom  8384  addcompq  8753  addcomnq  8754  mulcompq  8755  mulcomnq  8756  addassnq  8761  mulassnq  8762  addid1  9171  zeo  10280  xnegneg  10725  xaddcom  10749  xaddid1  10750  xnegdi  10752  xmulid1  10783  xadddilem  10798  ixxin  10858  fzsuc2  11028  expneg  11309  sq01  11421  facp1  11491  bcpasc  11532  hashf1lem1  11624  hashf1  11626  eqs1  11681  absexp  12029  sqreulem  12083  fsumf1o  12437  fsumadd  12452  fsumrev2  12485  fsumparts  12505  fsumrelem  12506  efexp  12622  tanval2  12654  sqr2irrlem  12767  sadeq  12904  smumullem  12924  smumul  12925  gcdcom  12940  gcd0id  12943  gcdass  12965  nn0gcdsq  13064  dfphi2  13083  pcneg  13167  setscom  13417  strfvi  13427  setsnid  13429  ressbas  13439  ressinbas  13445  ressress  13446  firest  13580  topnval  13582  xpsfeq  13709  xpsaddlem  13720  xpsvsca  13724  homffval  13837  oppchomfval  13860  oppcbas  13864  rescbas  13949  rescco  13952  cofuass  14006  fucbas  14077  fuchom  14078  setccatid  14159  xpcbas  14195  xpchomfval  14196  xpccofval  14199  oduleval  14478  oduglb  14486  odulub  14488  ipotset  14503  grpinvfvi  14766  symgbas  15015  symggrp  15023  cntrval  15038  cntzval  15040  oppgplusfval  15064  sylow1lem2  15153  sylow3lem1  15181  oppglsm  15196  gsumzsplit  15449  gsum2d  15466  gsumcom2  15469  dprd2dlem2  15518  dprd2da  15520  dmdprdsplit2lem  15523  mgpplusg  15572  mgpress  15579  rngidval  15586  opprmulfval  15650  abvtrivd  15848  sralem  16169  srasca  16173  sravsca  16174  rlmval  16184  psrmulr  16368  mplmonmul  16447  mplcoe3  16449  opsrbaslem  16458  opsrtoslem2  16465  psr1val  16504  ply1basfvi  16555  ply1plusgfvi  16556  psr1sca2  16565  zlmlem  16714  zlmsca  16718  zlmvsca  16719  ocvval  16810  thlbas  16839  thlle  16840  thloc  16842  tgdif0  16973  indislem  16980  restco  17143  txtopon  17537  txindislem  17579  qtopres  17644  hmphindis  17743  ptuncnv  17753  snclseqg  18059  tsmssplit  18095  ussval  18203  tuslem  18211  setsmsbas  18388  tnglem  18545  tngds  18553  tngtset  18554  pcoass  18913  cphsqrcl2  19013  ovolunlem1a  19252  ioorinv  19328  itg11  19443  itg1mulc  19456  itg2cnlem1  19513  iblss2  19557  ibladdlem  19571  itgfsum  19578  iblabslem  19579  iblabs  19580  ditgneg  19604  deg1fvi  19868  dgrco  20053  logfac  20355  cxpexp  20419  cxpmul2  20440  cxpsqr  20454  dvcxp2  20487  ang180lem1  20511  mcubic  20547  quart1  20556  reasinsin  20596  atanlogaddlem  20613  atantayl2  20638  log2tlbnd  20645  basellem2  20724  basellem3  20725  basellem5  20727  basellem8  20730  dchrmulid2  20896  bcp1ctr  20923  lgsneg  20963  lgsneg1  20964  lgsdir2  20972  lgsdir  20974  lgsdi  20976  lgsquad2lem2  21003  pntleml  21165  eupath2lem3  21542  bafval  21924  ipidsq  22050  ipasslem1  22173  pjclem2  23540  cvmdi  23668  imadifxp  23874  iundisjcnt  23985  indval2  24201  bayesth  24469  subfacp1lem6  24643  fprodf1o  25044  fprodmul  25056  fproddiv  25057  fprodfac  25068  fallfacfwd  25112  dfrdg2  25169  dfrdg3  25170  dfrdg4  25506  ordtoplem  25892  ordcmp  25904  itg2addnclem2  25951  ibladdnclem  25954  iblabsnclem  25961  iblabsnc  25962  iblmulc2nc  25963  kelac2  26825  dsmmval2  26864  m1expaddsub  27083  mendbas  27154  mendsca  27159  mendrng  27162  iotain  27279  addrcom  27341  itgsinexplem1  27409  dpfrac1  27854  pmodN  30015  tgrpgrplem  30914  tendoplass  30948  tendoicl  30961  erngdvlem3  31155  dvhvaddass  31263  dib0  31330  dib1dim2  31334  diclspsn  31360  cdlemn8  31370  dihopelvalcpre  31414  djhcom  31571
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 1661  ax-8 1682  ax-11 1753  ax-ext 2361
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2373
  Copyright terms: Public domain W3C validator