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

Theorem 3eqtr4ri 2466
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 2458 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2458 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652
This theorem is referenced by:  cbvreucsf  3305  dfin3  3572  dfif6  3734  qdass  3895  tpidm12  3897  unipr  4021  unidif0  4364  dfdm4  5055  dmun  5068  resres  5151  inres  5156  resiun1  5157  imainrect  5304  coundi  5363  coundir  5364  funopg  5477  offres  6311  1st2val  6364  2nd2val  6365  mpt2mptsx  6406  oeoalem  6831  omopthlem1  6890  snec  6959  tcsni  7674  infmap2  8090  ackbij2lem3  8113  itunisuc  8291  axmulass  9024  divmul13i  9767  dfnn3  10006  halfpm6th  10184  numsucc  10400  decbin2  10478  uzrdgxfr  11298  hashxplem  11688  ids1  11743  fsumadd  12524  fsum2d  12547  bezout  13034  ressbas  13511  oppchomf  13938  oppr1  15731  opsrtoslem1  16536  cnfldnm  18805  volres  19416  voliunlem1  19436  uniioombllem4  19470  itg11  19575  plyid  20120  coeidp  20173  dgrid  20174  dfrelog  20455  log2ublem3  20780  bposlem8  21067  ginvsn  21929  ip2i  22321  bcseqi  22614  hilnormi  22657  cmcmlem  23085  fh3i  23117  fh4i  23118  pjadjii  23168  ressplusf  24175  xpinpreima  24296  cnre2csqima  24301  ballotth  24787  fprodmul  25276  elrn3  25378  domep  25412  bpoly3  26096  itg2addnclem2  26247  stoweidlem13  27719  wallispi2  27779
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2416
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2428
  Copyright terms: Public domain W3C validator