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

Theorem 3eqtr4ri 2853
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 2845 . 2 𝐷 = 𝐴
4 3eqtr4i.2 . 2 𝐶 = 𝐴
53, 4eqtr4i 2845 1 𝐷 = 𝐶
Colors of variables: wff setvar class
Syntax hints:   = wceq 1530
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-9 2117  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-ex 1774  df-cleq 2812
This theorem is referenced by:  cbvreucsf  3925  dfin3  4241  dfsymdif3  4267  dfif6  4468  dfsn2ALT  4579  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  7191  elrnmpores  7280  offres  7676  1st2val  7709  2nd2val  7710  mpomptsx  7754  oeoalem  8214  omopthlem1  8274  snec  8352  tcsni  9177  infmap2  9632  ackbij2lem3  9655  itunisuc  9833  axmulass  10571  divmul13i  11393  dfnn3  11644  halfpm6th  11850  numsucc  12130  decbin2  12231  uzrdgxfr  13327  hashxplem  13786  prprrab  13823  ids1  13943  s3s4  14287  s2s5  14288  s5s2  14289  fsumadd  15088  fsum2d  15118  fprodmul  15306  bpoly3  15404  bezout  15883  ressbas  16546  oppchomf  16982  smndex1iidm  18058  symgbas  18491  oppr1  19376  opsrtoslem1  20256  m2detleiblem2  21229  txswaphmeolem  22404  cnfldnm  23379  cnrbas  23738  cnnm  23756  volres  24121  voliunlem1  24143  uniioombllem4  24179  itg11  24284  dfrelog  25141  log2ublem3  25518  bposlem8  25859  uhgrspan1  27077  ip2i  28597  bcseqi  28889  hilnormi  28932  cmcmlem  29360  fh3i  29392  fh4i  29393  pjadjii  29443  cnvoprabOLD  30448  resf1o  30458  dp3mul10  30567  dpmul4  30583  threehalves  30584  ressplusf  30630  cycpmconjs  30791  resvsca  30896  xpinpreima  31137  cnre2csqima  31142  esum2dlem  31339  eulerpartgbij  31618  ballotth  31783  plymulx  31806  hgt750lem2  31911  elrn3  32986  itg2addnclem2  34931  dfcoss3  35649  cossid  35707  dfssr2  35726  rabdif  39092  areaquad  39808  cnvrcl0  39970  stoweidlem13  42283  wallispi2  42343  fourierdlem96  42472  fourierdlem97  42473  fourierdlem98  42474  fourierdlem99  42475  fourierdlem113  42489  fourierswlem  42500  dfafv2  43316  dfnelbr2  43457  fmtnorec2  43690  fmtno5fac  43729  setrec2  44783
  Copyright terms: Public domain W3C validator