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

Theorem 3eqtr4ri 2443
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 2435 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2435 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  cbvreucsf  3281  dfin3  3548  dfif6  3710  qdass  3871  tpidm12  3873  unipr  3997  unidif0  4340  dfdm4  5030  dmun  5043  resres  5126  inres  5131  resiun1  5132  imainrect  5279  coundi  5338  coundir  5339  funopg  5452  offres  6286  1st2val  6339  2nd2val  6340  mpt2mptsx  6381  oeoalem  6806  omopthlem1  6865  snec  6934  tcsni  7646  infmap2  8062  ackbij2lem3  8085  itunisuc  8263  axmulass  8996  divmul13i  9739  dfnn3  9978  halfpm6th  10156  numsucc  10372  decbin2  10450  uzrdgxfr  11269  hashxplem  11659  ids1  11714  fsumadd  12495  fsum2d  12518  bezout  13005  ressbas  13482  oppchomf  13909  oppr1  15702  opsrtoslem1  16507  cnfldnm  18774  volres  19385  voliunlem1  19405  uniioombllem4  19439  itg11  19544  plyid  20089  coeidp  20142  dgrid  20143  dfrelog  20424  log2ublem3  20749  bposlem8  21036  ginvsn  21898  ip2i  22290  bcseqi  22583  hilnormi  22626  cmcmlem  23054  fh3i  23086  fh4i  23087  pjadjii  23137  ressplusf  24144  xpinpreima  24265  cnre2csqima  24270  ballotth  24756  fprodmul  25245  elrn3  25342  domep  25371  bpoly3  26016  itg2addnclem2  26164  stoweidlem13  27637  wallispi2  27697
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 2393
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2405
  Copyright terms: Public domain W3C validator