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

Theorem 3eqtr4ri 2852
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 𝐴 = 𝐵
3eqtr4i.2 𝐶 = 𝐴
3eqtr4i.3 𝐷 = 𝐵
Assertion
Ref Expression
3eqtr4ri 𝐷 = 𝐶

Proof of Theorem 3eqtr4ri
StepHypRef Expression
1 3eqtr4i.3 . . 3 𝐷 = 𝐵
2 3eqtr4i.1 . . 3 𝐴 = 𝐵
31, 2eqtr4i 2844 . 2 𝐷 = 𝐴
4 3eqtr4i.2 . 2 𝐶 = 𝐴
53, 4eqtr4i 2844 1 𝐷 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-9 2115  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1772  df-cleq 2811
This theorem is referenced by:  cbvreucsf  3924  dfin3  4240  dfsymdif3  4266  dfif6  4466  dfsn2ALT  4577  qdass  4681  tpidm12  4683  unipr  4843  iinvdif  4993  unidif0  5251  csbcnv  5747  dfdm4  5757  dmun  5772  domepOLD  5787  resres  5859  inres  5864  resdifcom  5865  resiun1  5866  imainrect  6031  cnvcnv  6042  coundi  6093  coundir  6094  funopg  6382  csbov  7188  elrnmpores  7277  offres  7673  1st2val  7706  2nd2val  7707  mpomptsx  7751  oeoalem  8211  omopthlem1  8271  snec  8349  tcsni  9173  infmap2  9628  ackbij2lem3  9651  itunisuc  9829  axmulass  10567  divmul13i  11389  dfnn3  11640  halfpm6th  11846  numsucc  12126  decbin2  12227  uzrdgxfr  13323  hashxplem  13782  prprrab  13819  ids1  13939  s3s4  14283  s2s5  14284  s5s2  14285  fsumadd  15084  fsum2d  15114  fprodmul  15302  bpoly3  15400  bezout  15879  ressbas  16542  oppchomf  16978  oppr1  19313  opsrtoslem1  20192  m2detleiblem2  21165  txswaphmeolem  22340  cnfldnm  23314  cnrbas  23673  cnnm  23691  volres  24056  voliunlem1  24078  uniioombllem4  24114  itg11  24219  dfrelog  25076  log2ublem3  25453  bposlem8  25794  uhgrspan1  27012  ip2i  28532  bcseqi  28824  hilnormi  28867  cmcmlem  29295  fh3i  29327  fh4i  29328  pjadjii  29378  cnvoprabOLD  30382  resf1o  30392  dp3mul10  30501  dpmul4  30517  threehalves  30518  ressplusf  30564  cycpmconjs  30725  resvsca  30830  xpinpreima  31048  cnre2csqima  31053  esum2dlem  31250  eulerpartgbij  31529  ballotth  31694  plymulx  31717  hgt750lem2  31822  elrn3  32895  itg2addnclem2  34825  dfcoss3  35542  cossid  35600  dfssr2  35619  rabdif  38985  areaquad  39701  cnvrcl0  39863  stoweidlem13  42175  wallispi2  42235  fourierdlem96  42364  fourierdlem97  42365  fourierdlem98  42366  fourierdlem99  42367  fourierdlem113  42381  fourierswlem  42392  dfafv2  43208  dfnelbr2  43349  fmtnorec2  43582  fmtno5fac  43621  smndex1iidm  44001  setrec2  44726
  Copyright terms: Public domain W3C validator