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

Theorem 3eqtr4ri 2327
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 2319 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2319 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1632
This theorem is referenced by:  cbvreucsf  3158  dfin3  3421  dfif6  3581  qdass  3739  tpidm12  3741  unipr  3857  unidif0  4199  dfdm4  4888  dmun  4901  resres  4984  inres  4989  resiun1  4990  imainrect  5135  coundi  5190  coundir  5191  funopg  5302  offres  6108  1st2val  6161  2nd2val  6162  mpt2mptsx  6203  oeoalem  6610  omopthlem1  6669  snec  6738  tcsni  7444  infmap2  7860  ackbij2lem3  7883  itunisuc  8061  axmulass  8795  divmul13i  9537  dfnn3  9776  halfpm6th  9952  numsucc  10166  decbin2  10244  uzrdgxfr  11045  hashxplem  11401  ids1  11453  fsumadd  12227  fsum2d  12250  bezout  12737  ressbas  13214  oppr1  15432  opsrtoslem1  16241  cnfldnm  18304  volres  18903  voliunlem1  18923  uniioombllem4  18957  itg11  19062  plyid  19607  coeidp  19660  dgrid  19661  dfrelog  19939  log2ublem3  20260  bposlem8  20546  ginvsn  21032  ip2i  21422  bcseqi  21715  hilnormi  21758  cmcmlem  22186  fh3i  22218  fh4i  22219  pjadjii  22269  ballotth  23112  xpinpreima  23305  cnre2csqima  23310  ressplusf  23313  elrn3  24191  domep  24220  bpoly3  24865  itg2addnclem2  25004  empos  25345  stoweidlem13  27865
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-11 1727  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-cleq 2289
  Copyright terms: Public domain W3C validator