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

Theorem 3eqtr4ri 2314
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 2306 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2306 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1623
This theorem is referenced by:  cbvreucsf  3145  dfin3  3408  dfif6  3568  qdass  3726  tpidm12  3728  unipr  3841  unidif0  4183  dfdm4  4872  dmun  4885  resres  4968  inres  4973  resiun1  4974  imainrect  5119  coundi  5174  coundir  5175  funopg  5286  offres  6092  1st2val  6145  2nd2val  6146  mpt2mptsx  6187  oeoalem  6594  omopthlem1  6653  snec  6722  tcsni  7428  infmap2  7844  ackbij2lem3  7867  itunisuc  8045  axmulass  8779  divmul13i  9521  dfnn3  9760  halfpm6th  9936  numsucc  10150  decbin2  10228  uzrdgxfr  11029  hashxplem  11385  ids1  11437  fsumadd  12211  fsum2d  12234  bezout  12721  ressbas  13198  oppr1  15416  opsrtoslem1  16225  cnfldnm  18288  volres  18887  voliunlem1  18907  uniioombllem4  18941  itg11  19046  plyid  19591  coeidp  19644  dgrid  19645  dfrelog  19923  log2ublem3  20244  bposlem8  20530  ginvsn  21016  ip2i  21406  bcseqi  21699  hilnormi  21742  cmcmlem  22170  fh3i  22202  fh4i  22203  pjadjii  22253  ballotth  23096  xpinpreima  23290  cnre2csqima  23295  ressplusf  23298  elrn3  24120  domep  24149  bpoly3  24793  empos  25242  stoweidlem13  27762
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-11 1715  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-cleq 2276
  Copyright terms: Public domain W3C validator