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

Theorem 3eqtr4a 2499
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 2489 . 2  |-  ( ph  ->  C  =  B )
4 3eqtr4a.3 . 2  |-  ( ph  ->  D  =  B )
53, 4eqtr4d 2476 1  |-  ( ph  ->  C  =  D )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1364
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-12 1797  ax-ext 2422
This theorem depends on definitions:  df-bi 185  df-ex 1592  df-cleq 2434
This theorem is referenced by:  rabsnif  3941  uniintsn  4162  iinvdif  4239  iununi  4252  unizlim  4831  dmxpid  5055  rnxpid  5268  csbrn  5296  dmsnsnsn  5314  opswap  5323  xpcoid  5375  fvco4i  5766  fndmdifcom  5805  fmptsng  5897  csbov  6122  ordunisuc  6442  offres  6571  1stval2  6593  2ndval2  6594  cnvf1olem  6669  fparlem3  6673  fparlem4  6674  imacosupp  6728  seqomlem1  6901  ecovcom  7207  ecovass  7208  ecovdi  7209  resixpfo  7297  mapunen  7476  cardidm  8125  cardiun  8148  alephcard  8236  cardalephex  8256  cardcf  8417  cfidm  8440  alephsing  8441  itunisuc  8584  itunitc  8586  ituniiun  8587  alephadd  8737  alephreg  8742  pwcfsdom  8743  addcompq  9115  addcomnq  9116  mulcompq  9117  mulcomnq  9118  addassnq  9123  mulassnq  9124  addid1  9545  zeo  10723  xnegneg  11180  xaddcom  11204  xaddid1  11205  xnegdi  11207  xmulid1  11238  xadddilem  11253  ixxin  11313  fzsuc2  11510  expneg  11869  sq01  11982  facp1  12052  bcpasc  12093  hashf1lem1  12204  hashf1  12206  eqs1  12296  swrdccatin1  12370  swrdccat3blem  12382  repswsymballbi  12414  cshwmodn  12428  repswcshw  12442  absexp  12789  sqreulem  12843  fsumf1o  13196  fsumadd  13211  fsumrev2  13245  fsumparts  13265  fsumrelem  13266  efexp  13381  tanval2  13413  sqr2irrlem  13526  sadeq  13664  smumullem  13684  smumul  13685  gcdcom  13700  gcd0id  13703  gcdass  13725  nn0gcdsq  13826  dfphi2  13845  pcneg  13936  setscom  14200  strfvi  14210  setsnid  14212  ressbas  14224  ressinbas  14230  ressress  14231  firest  14367  topnval  14369  xpsfeq  14498  xpsaddlem  14509  xpsvsca  14513  homffval  14626  oppchomfval  14649  oppcbas  14653  rescbas  14738  rescco  14741  cofuass  14795  fucbas  14866  fuchom  14867  setccatid  14948  xpcbas  14984  xpchomfval  14985  xpccofval  14988  oduleval  15297  oduglb  15305  odulub  15307  ipotset  15323  grpinvfvi  15572  cntrval  15830  cntzval  15832  oppgplusfval  15856  symgbas  15878  symggrp  15898  pmtrprfval  15986  m1expaddsub  15997  sylow1lem2  16091  sylow3lem1  16119  oppglsm  16134  gsumzsplit  16411  gsumzsplitOLD  16412  gsum2dlem2  16452  gsum2dOLD  16454  gsumcom2  16457  dprd2dlem2  16529  dprd2da  16531  dmdprdsplit2lem  16534  mgpplusg  16585  mgpress  16592  rngidval  16595  opprmulfval  16707  abvtrivd  16905  sralem  17236  srasca  17240  sravsca  17241  sraip  17242  rlmval  17250  psrmulr  17433  mplmonmul  17521  mplcoe3  17523  mplcoe3OLD  17524  opsrbaslem  17535  opsrtoslem2  17542  psr1val  17618  ply1basfvi  17671  ply1plusgfvi  17672  psr1sca2  17681  evl1fval1lem  17734  zlmlem  17907  zlmsca  17911  zlmvsca  17912  psgninv  17971  ocvval  18051  thlbas  18080  thlle  18081  thloc  18083  dsmmval2  18120  mattpos1  18299  mdettpos  18376  smadiadetglem1  18436  tgdif0  18556  indislem  18563  restco  18727  txtopon  19123  txindislem  19165  qtopres  19230  hmphindis  19329  ptuncnv  19339  snclseqg  19645  tsmssplit  19685  ussval  19793  tuslem  19801  setsmsbas  20009  tnglem  20185  tngds  20193  tngtset  20194  pcoass  20555  cphsqrcl2  20664  rrxcph  20855  ovolunlem1a  20938  ioorinv  21015  itg11  21128  itg1mulc  21141  itg2cnlem1  21198  iblss2  21242  ibladdlem  21256  itgfsum  21263  iblabslem  21264  iblabs  21265  ditgneg  21291  deg1fvi  21515  dgrco  21701  logfac  22008  cxpexp  22072  cxpmul2  22093  cxpsqr  22107  dvcxp2  22140  ang180lem1  22164  mcubic  22201  quart1  22210  reasinsin  22250  atanlogaddlem  22267  atantayl2  22292  log2tlbnd  22299  basellem2  22378  basellem3  22379  basellem5  22381  basellem8  22384  dchrmulid2  22550  bcp1ctr  22577  lgsneg  22617  lgsneg1  22618  lgsdir2  22626  lgsdir  22628  lgsdi  22630  lgsquad2lem2  22657  pntleml  22819  ttglem  23057  eupath2lem3  23535  bafval  23917  ipidsq  24043  ipasslem1  24166  pjclem2  25535  cvmdi  25663  imadifxp  25874  iundisjcnt  26015  resvsca  26234  indval2  26407  bayesth  26752  subfacp1lem6  27003  fprodf1o  27388  fprodmul  27400  fproddiv  27401  fprodfac  27412  fallfacfwd  27468  dfrdg2  27538  dfrdg3  27539  dfrdg4  27910  ordtoplem  28211  ordcmp  28223  mblfinlem2  28354  itg2addnclem2  28369  ibladdnclem  28373  iblabsnclem  28380  iblabsnc  28381  iblmulc2nc  28382  ftc1anclem8  28399  kelac2  29343  mendbas  29466  mendsca  29471  mendrng  29474  iotain  29596  addrcom  29656  itgsinexplem1  29719  fmptsnd  30646  dpfrac1  30948  pmodN  33216  tgrpgrplem  34115  tendoplass  34149  tendoicl  34162  erngdvlem3  34356  dvhvaddass  34464  dib0  34531  dib1dim2  34535  diclspsn  34561  cdlemn8  34571  dihopelvalcpre  34615  djhcom  34772
  Copyright terms: Public domain W3C validator