MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  3eqtr4ri Structured 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 1398
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-cleq 2446
This theorem is referenced by:  cbvreucsf  3454  dfin3  3734  dfsymdif3  3760  dfif6  3932  qdass  4115  tpidm12  4117  unipr  4248  iinvdif  4387  unidif0  4610  csbcnv  5175  dfdm4  5184  dmun  5198  resres  5274  inres  5279  resiun1  5280  imainrect  5433  coundi  5491  coundir  5492  funopg  5602  csbov  6305  elrnmpt2res  6389  offres  6768  1st2val  6799  2nd2val  6800  mpt2mptsx  6836  oeoalem  7237  omopthlem1  7296  snec  7366  tcsni  8165  infmap2  8589  ackbij2lem3  8612  itunisuc  8790  axmulass  9523  divmul13i  10301  dfnn3  10545  halfpm6th  10756  numsucc  11002  decbin2  11080  uzrdgxfr  12059  hashxplem  12475  ids1  12598  fsumadd  13643  fsum2d  13668  fprodmul  13847  bezout  14264  ressbas  14773  oppchomf  15208  oppr1  17478  opsrtoslem1  18343  m2detleiblem2  19297  cnfldnm  21452  volres  22105  voliunlem1  22126  uniioombllem4  22161  itg11  22264  plyid  22772  coeidp  22826  dgrid  22827  dfrelog  23119  log2ublem3  23476  bposlem8  23764  ginvsn  25549  ip2i  25941  bcseqi  26235  hilnormi  26278  cmcmlem  26707  fh3i  26739  fh4i  26740  pjadjii  26790  cnvoprab  27777  resf1o  27784  ressplusf  27872  resvsca  28055  xpinpreima  28123  cnre2csqima  28128  esum2dlem  28321  eulerpartgbij  28575  ballotth  28740  plymulx  28769  elrn3  29433  domep  29465  bpoly3  30048  itg2addnclem2  30307  areaquad  31425  stoweidlem13  32034  wallispi2  32094  fourierdlem96  32224  fourierdlem97  32225  fourierdlem98  32226  fourierdlem99  32227  fourierdlem113  32241  fourierswlem  32252
  Copyright terms: Public domain W3C validator