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

Theorem 3eqtr4ri 2507
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 2499 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2499 1  |-  D  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-cleq 2459
This theorem is referenced by:  cbvreucsf  3469  dfin3  3737  dfif6  3942  qdass  4126  tpidm12  4128  unipr  4258  iinvdif  4397  unidif0  4620  csbcnv  5186  dfdm4  5195  dmun  5209  resres  5286  inres  5291  resiun1  5292  imainrect  5448  coundi  5508  coundir  5509  funopg  5620  csbov  6317  elrnmpt2res  6401  offres  6780  1st2val  6811  2nd2val  6812  mpt2mptsx  6848  oeoalem  7246  omopthlem1  7305  snec  7375  tcsni  8175  infmap2  8599  ackbij2lem3  8622  itunisuc  8800  axmulass  9535  divmul13i  10306  dfnn3  10551  halfpm6th  10761  numsucc  11003  decbin2  11081  uzrdgxfr  12046  hashxplem  12458  ids1  12575  fsumadd  13527  fsum2d  13552  bezout  14042  ressbas  14548  oppchomf  14979  oppr1  17096  opsrtoslem1  17959  m2detleiblem2  18937  cnfldnm  21113  volres  21766  voliunlem1  21787  uniioombllem4  21822  itg11  21925  plyid  22433  coeidp  22486  dgrid  22487  dfrelog  22778  log2ublem3  23104  bposlem8  23391  ginvsn  25124  ip2i  25516  bcseqi  25810  hilnormi  25853  cmcmlem  26282  fh3i  26314  fh4i  26315  pjadjii  26365  cnvoprab  27315  resf1o  27322  ressplusf  27397  resvsca  27580  xpinpreima  27639  cnre2csqima  27644  eulerpartgbij  28062  ballotth  28227  plymulx  28256  fprodmul  28943  elrn3  29045  domep  29078  bpoly3  29673  itg2addnclem2  29920  areaquad  31016  stoweidlem13  31540  wallispi2  31600  fourierdlem113  31747
  Copyright terms: Public domain W3C validator