Theorem 3eqtr4ri 2763

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

Step	Hyp	Ref	Expression
1		3eqtr4i.3	. . 3 ⊢ 𝐷 = 𝐵
2		3eqtr4i.1	. . 3 ⊢ 𝐴 = 𝐵
3	1, 2	eqtr4i 2755	. 2 ⊢ 𝐷 = 𝐴
4		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
5	3, 4	eqtr4i 2755	1 ⊢ 𝐷 = 𝐶

Syntax hints:   = wceq 1540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1780  df-cleq 2721

This theorem is referenced by:  cbvreucsf  3895  dfin3  4228  dfsymdif3  4257  rabdif  4272  dfif6  4479  dfsn2ALT  4599  qdass  4705  tpidm12  4707  iinvdif  5029  unidif0  5299  csbcnv  5826  dfdm4  5838  dmun  5853  resres  5943  inres  5948  resdifcom  5949  resiun1  5950  imainrect  6130  cnvcnv  6141  coundi  6196  coundir  6197  funopg  6516  csbov  7394  elrnmpores  7487  offres  7918  1st2val  7952  2nd2val  7953  mpomptsx  7999  oeoalem  8514  omopthlem1  8577  snec  8705  tcsni  9639  infmap2  10111  ackbij2lem3  10134  itunisuc  10313  axmulass  11051  divmul13i  11885  dfnn3  12142  numsucc  12631  decbin2  12732  uzrdgxfr  13874  hashxplem  14340  prprrab  14380  ids1  14504  s3s4  14840  s2s5  14841  s5s2  14842  fsumadd  15647  fsum2d  15678  fprodmul  15867  bpoly3  15965  bezout  16454  oppchomf  17626  dfinito3  17912  dftermo3  17913  smndex1iidm  18775  symgbas  19251  oppr1  20235  opsrtoslem1  21960  m2detleiblem2  22513  txswaphmeolem  23689  cnfldnm  24664  cnrbas  25040  cnnm  25058  volres  25427  voliunlem1  25449  uniioombllem4  25485  itg11  25590  dfrelog  26472  log2ublem3  26856  bposlem8  27200  noinfbnd2  27641  addsasslem1  27915  uhgrspan1  29248  ip2i  30772  bcseqi  31064  hilnormi  31107  cmcmlem  31535  fh3i  31567  fh4i  31568  pjadjii  31618  resf1o  32673  dp3mul10  32838  dpmul4  32854  threehalves  32855  ressplusf  32905  cycpmconjs  33098  resvsca  33270  cos9thpiminplylem5  33753  xpinpreima  33873  cnre2csqima  33878  esum2dlem  34059  eulerpartgbij  34340  ballotth  34506  plymulx  34516  hgt750lem2  34620  elrn3  35739  itg2addnclem2  37656  dfcoss3  38395  cossid  38461  dfssr2  38480  areaquad  43193  cnvrcl0  43602  stoweidlem13  45998  wallispi2  46058  fourierdlem96  46187  fourierdlem97  46188  fourierdlem98  46189  fourierdlem99  46190  fourierdlem113  46204  fourierswlem  46215  dfafv2  47120  dfnelbr2  47261  ceil5half3  47328  fmtnorec2  47531  fmtno5fac  47570  tposrescnv  48867  tposres3  48869  dfswapf2  49250  setrec2  49684