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

Theorem 3eqtr4ri 2467
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 2459 . 2  |-  D  =  A
4 3eqtr4i.2 . 2  |-  C  =  A
53, 4eqtr4i 2459 1  |-  D  =  C
Colors of variables: wff set class
Syntax hints:    = wceq 1652
This theorem is referenced by:  cbvreucsf  3313  dfin3  3580  dfif6  3742  qdass  3903  tpidm12  3905  unipr  4029  unidif0  4372  dfdm4  5063  dmun  5076  resres  5159  inres  5164  resiun1  5165  imainrect  5312  coundi  5371  coundir  5372  funopg  5485  offres  6319  1st2val  6372  2nd2val  6373  mpt2mptsx  6414  oeoalem  6839  omopthlem1  6898  snec  6967  tcsni  7682  infmap2  8098  ackbij2lem3  8121  itunisuc  8299  axmulass  9032  divmul13i  9775  dfnn3  10014  halfpm6th  10192  numsucc  10408  decbin2  10486  uzrdgxfr  11306  hashxplem  11696  ids1  11751  fsumadd  12532  fsum2d  12555  bezout  13042  ressbas  13519  oppchomf  13946  oppr1  15739  opsrtoslem1  16544  cnfldnm  18813  volres  19424  voliunlem1  19444  uniioombllem4  19478  itg11  19583  plyid  20128  coeidp  20181  dgrid  20182  dfrelog  20463  log2ublem3  20788  bposlem8  21075  ginvsn  21937  ip2i  22329  bcseqi  22622  hilnormi  22665  cmcmlem  23093  fh3i  23125  fh4i  23126  pjadjii  23176  ressplusf  24183  xpinpreima  24304  cnre2csqima  24309  ballotth  24795  fprodmul  25284  elrn3  25386  domep  25420  bpoly3  26104  itg2addnclem2  26257  stoweidlem13  27738  wallispi2  27798
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-11 1761  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-ex 1551  df-cleq 2429
  Copyright terms: Public domain W3C validator