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

Theorem 3eqtr4ri 2481
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 2473 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2473 1  |-  D  =  C
Colors of variables: wff setvar class
Syntax hints:    = wceq 1381
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-cleq 2433
This theorem is referenced by:  cbvreucsf  3452  dfin3  3720  dfif6  3926  qdass  4111  tpidm12  4113  unipr  4244  iinvdif  4384  unidif0  4607  csbcnv  5173  dfdm4  5182  dmun  5196  resres  5273  inres  5278  resiun1  5279  imainrect  5435  coundi  5495  coundir  5496  funopg  5607  csbov  6313  elrnmpt2res  6398  offres  6777  1st2val  6808  2nd2val  6809  mpt2mptsx  6845  oeoalem  7244  omopthlem1  7303  snec  7373  tcsni  8174  infmap2  8598  ackbij2lem3  8621  itunisuc  8799  axmulass  9534  divmul13i  10308  dfnn3  10553  halfpm6th  10763  numsucc  11007  decbin2  11085  uzrdgxfr  12053  hashxplem  12467  ids1  12585  fsumadd  13537  fsum2d  13562  bezout  14054  ressbas  14561  oppchomf  14989  oppr1  17154  opsrtoslem1  18019  m2detleiblem2  19000  cnfldnm  21156  volres  21809  voliunlem1  21830  uniioombllem4  21865  itg11  21968  plyid  22476  coeidp  22529  dgrid  22530  dfrelog  22822  log2ublem3  23148  bposlem8  23435  ginvsn  25220  ip2i  25612  bcseqi  25906  hilnormi  25949  cmcmlem  26378  fh3i  26410  fh4i  26411  pjadjii  26461  cnvoprab  27415  resf1o  27422  ressplusf  27508  resvsca  27690  xpinpreima  27758  cnre2csqima  27763  eulerpartgbij  28181  ballotth  28346  plymulx  28375  fprodmul  29062  elrn3  29164  domep  29197  bpoly3  29792  itg2addnclem2  30039  areaquad  31157  stoweidlem13  31684  wallispi2  31744  fourierdlem96  31874  fourierdlem97  31875  fourierdlem98  31876  fourierdlem99  31877  fourierdlem113  31891  fourierswlem  31902
  Copyright terms: Public domain W3C validator