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

Theorem 3eqtr4ri 2494
Description: An inference from three chained equalities. (Contributed by NM, 2-Sep-1995.) (Proof shortened by Andrew Salmon, 25-May-2011.)
Hypotheses
Ref Expression
3eqtr4i.1  |-  A  =  B
3eqtr4i.2  |-  C  =  A
3eqtr4i.3  |-  D  =  B
Assertion
Ref Expression
3eqtr4ri  |-  D  =  C

Proof of Theorem 3eqtr4ri
StepHypRef Expression
1 3eqtr4i.3 . . 3  |-  D  =  B
2 3eqtr4i.1 . . 3  |-  A  =  B
31, 2eqtr4i 2486 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2486 1  |-  D  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  cbvreucsf  3432  dfin3  3700  dfif6  3905  qdass  4085  tpidm12  4087  unipr  4215  iinvdif  4353  unidif0  4576  csbcnv  5134  dfdm4  5143  dmun  5157  resres  5234  inres  5239  resiun1  5240  imainrect  5390  coundi  5450  coundir  5451  funopg  5561  csbov  6235  elrnmpt2res  6317  offres  6685  1st2val  6715  2nd2val  6716  mpt2mptsx  6750  oeoalem  7148  omopthlem1  7207  snec  7276  tcsni  8077  infmap2  8501  ackbij2lem3  8524  itunisuc  8702  axmulass  9438  divmul13i  10206  dfnn3  10450  halfpm6th  10660  numsucc  10895  decbin2  10973  uzrdgxfr  11909  hashxplem  12316  ids1  12410  fsumadd  13336  fsum2d  13359  bezout  13847  ressbas  14350  oppchomf  14781  oppr1  16852  opsrtoslem1  17692  m2detleiblem2  18569  cnfldnm  20493  volres  21146  voliunlem1  21167  uniioombllem4  21202  itg11  21305  plyid  21813  coeidp  21866  dgrid  21867  dfrelog  22153  log2ublem3  22479  bposlem8  22766  ginvsn  24008  ip2i  24400  bcseqi  24694  hilnormi  24737  cmcmlem  25166  fh3i  25198  fh4i  25199  pjadjii  25249  cnvoprab  26194  resf1o  26201  ressplusf  26276  resvsca  26463  xpinpreima  26501  cnre2csqima  26506  eulerpartgbij  26919  ballotth  27084  plymulx  27113  fprodmul  27635  elrn3  27737  domep  27770  bpoly3  28365  itg2addnclem2  28612  areaquad  29760  stoweidlem13  29976  wallispi2  30036
  Copyright terms: Public domain W3C validator