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

Theorem 3eqtr4ri 2420
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 2412 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2412 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1649
This theorem is referenced by:  cbvreucsf  3258  dfin3  3525  dfif6  3687  qdass  3848  tpidm12  3850  unipr  3973  unidif0  4315  dfdm4  5005  dmun  5018  resres  5101  inres  5106  resiun1  5107  imainrect  5254  coundi  5313  coundir  5314  funopg  5427  offres  6260  1st2val  6313  2nd2val  6314  mpt2mptsx  6355  oeoalem  6777  omopthlem1  6836  snec  6905  tcsni  7617  infmap2  8033  ackbij2lem3  8056  itunisuc  8234  axmulass  8967  divmul13i  9709  dfnn3  9948  halfpm6th  10126  numsucc  10342  decbin2  10420  uzrdgxfr  11235  hashxplem  11625  ids1  11680  fsumadd  12461  fsum2d  12484  bezout  12971  ressbas  13448  oppchomf  13875  oppr1  15668  opsrtoslem1  16473  cnfldnm  18686  volres  19293  voliunlem1  19313  uniioombllem4  19347  itg11  19452  plyid  19997  coeidp  20050  dgrid  20051  dfrelog  20332  log2ublem3  20657  bposlem8  20944  ginvsn  21787  ip2i  22179  bcseqi  22472  hilnormi  22515  cmcmlem  22943  fh3i  22975  fh4i  22976  pjadjii  23026  ressplusf  24024  xpinpreima  24110  cnre2csqima  24115  ballotth  24576  fprodmul  25065  elrn3  25146  domep  25175  bpoly3  25820  itg2addnclem2  25960  stoweidlem13  27432  wallispi2  27492
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 2370
This theorem depends on definitions:  df-bi 178  df-ex 1548  df-cleq 2382
  Copyright terms: Public domain W3C validator