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

Theorem 3eqtr4ri 2494
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 2486 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2486 1  |-  D  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1454
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-ext 2441
This theorem depends on definitions:  df-bi 190  df-cleq 2454
This theorem is referenced by:  cbvreucsf  3408  dfin3  3693  dfsymdif3  3719  dfif6  3895  qdass  4083  tpidm12  4085  unipr  4224  iinvdif  4363  unidif0  4589  csbcnv  5036  dfdm4  5045  dmun  5059  resres  5135  inres  5140  resiun1  5141  imainrect  5296  coundi  5354  coundir  5355  funopg  5632  csbov  6349  elrnmpt2res  6436  offres  6814  1st2val  6845  2nd2val  6846  mpt2mptsx  6882  oeoalem  7322  omopthlem1  7381  snec  7451  tcsni  8252  infmap2  8673  ackbij2lem3  8696  itunisuc  8874  axmulass  9606  divmul13i  10395  dfnn3  10650  halfpm6th  10862  numsucc  11105  decbin2  11183  uzrdgxfr  12211  hashxplem  12637  ids1  12771  fsumadd  13853  fsum2d  13880  fprodmul  14062  bpoly3  14159  bezout  14558  ressbas  15227  oppchomf  15673  oppr1  17910  opsrtoslem1  18755  m2detleiblem2  19701  cnfldnm  21847  volres  22530  voliunlem1  22551  uniioombllem4  22592  itg11  22697  plyid  23211  coeidp  23265  dgrid  23266  dfrelog  23563  log2ublem3  23922  bposlem8  24267  ginvsn  26125  ip2i  26517  bcseqi  26821  hilnormi  26864  cmcmlem  27292  fh3i  27324  fh4i  27325  pjadjii  27375  cnvoprab  28356  resf1o  28363  ressplusf  28459  resvsca  28641  xpinpreima  28760  cnre2csqima  28765  esum2dlem  28961  eulerpartgbij  29253  ballotth  29418  ballotthOLD  29456  plymulx  29485  elrn3  30451  domep  30487  itg2addnclem2  32038  areaquad  36145  cnvrcl0  36276  stoweidlem13  37910  wallispi2  37972  fourierdlem96  38103  fourierdlem97  38104  fourierdlem98  38105  fourierdlem99  38106  fourierdlem113  38120  fourierswlem  38131  prprrab  39113  uhgrspan1  39424
  Copyright terms: Public domain W3C validator