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

Theorem 3eqtr4ri 2463
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 2455 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2455 1  |-  D  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1438
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-cleq 2415
This theorem is referenced by:  cbvreucsf  3430  dfin3  3713  dfsymdif3  3739  dfif6  3913  qdass  4097  tpidm12  4099  unipr  4230  iinvdif  4369  unidif0  4595  csbcnv  5035  dfdm4  5044  dmun  5058  resres  5134  inres  5139  resiun1  5140  imainrect  5295  coundi  5353  coundir  5354  funopg  5631  csbov  6338  elrnmpt2res  6422  offres  6800  1st2val  6831  2nd2val  6832  mpt2mptsx  6868  oeoalem  7303  omopthlem1  7362  snec  7432  tcsni  8230  infmap2  8650  ackbij2lem3  8673  itunisuc  8851  axmulass  9583  divmul13i  10370  dfnn3  10625  halfpm6th  10836  numsucc  11079  decbin2  11157  uzrdgxfr  12181  hashxplem  12604  ids1  12734  fsumadd  13798  fsum2d  13825  fprodmul  14007  bpoly3  14104  bezout  14503  ressbas  15172  oppchomf  15618  oppr1  17855  opsrtoslem1  18700  m2detleiblem2  19645  cnfldnm  21791  volres  22474  voliunlem1  22495  uniioombllem4  22536  itg11  22641  plyid  23155  coeidp  23209  dgrid  23210  dfrelog  23507  log2ublem3  23866  bposlem8  24211  ginvsn  26069  ip2i  26461  bcseqi  26765  hilnormi  26808  cmcmlem  27236  fh3i  27268  fh4i  27269  pjadjii  27319  cnvoprab  28308  resf1o  28315  ressplusf  28412  resvsca  28595  xpinpreima  28714  cnre2csqima  28719  esum2dlem  28915  eulerpartgbij  29207  ballotth  29372  ballotthOLD  29410  plymulx  29439  elrn3  30404  domep  30440  itg2addnclem2  31952  areaquad  36065  stoweidlem13  37737  wallispi2  37799  fourierdlem96  37930  fourierdlem97  37931  fourierdlem98  37932  fourierdlem99  37933  fourierdlem113  37947  fourierswlem  37958
  Copyright terms: Public domain W3C validator