Theorem 3eqtr4ri 2771

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 2763	. 2 ⊢ 𝐷 = 𝐴
4		3eqtr4i.2	. 2 ⊢ 𝐶 = 𝐴
5	3, 4	eqtr4i 2763	1 ⊢ 𝐷 = 𝐶

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  cbvreucsf  3882  dfin3  4218  dfsymdif3  4247  rabdif  4262  dfif6  4470  dfsn2ALT  4590  qdass  4698  tpidm12  4700  iinvdif  5023  unidif0  5298  csbcnv  5833  dfdm4  5845  dmun  5860  resres  5952  inres  5957  resdifcom  5958  resiun1  5959  imainrect  6140  cnvcnv  6151  coundi  6206  coundir  6207  funopg  6527  csbov  7406  elrnmpores  7499  offres  7930  1st2val  7964  2nd2val  7965  mpomptsx  8011  oeoalem  8526  omopthlem1  8589  snec  8719  tcsni  9656  infmap2  10133  ackbij2lem3  10156  itunisuc  10335  axmulass  11074  divmul13i  11910  dfnn3  12182  numsucc  12678  decbin2  12779  uzrdgxfr  13923  hashxplem  14389  prprrab  14429  ids1  14554  s3s4  14889  s2s5  14890  s5s2  14891  fsumadd  15696  fsum2d  15727  fprodmul  15919  bpoly3  16017  bezout  16506  oppchomf  17680  dfinito3  17966  dftermo3  17967  smndex1iidm  18863  symgbas  19341  oppr1  20324  opsrtoslem1  22046  m2detleiblem2  22606  txswaphmeolem  23782  cnfldnm  24756  cnrbas  25122  cnnm  25140  volres  25508  voliunlem1  25530  uniioombllem4  25566  itg11  25671  dfrelog  26545  log2ublem3  26928  bposlem8  27271  noinfbnd2  27712  addsasslem1  28012  bdaypw2n0bndlem  28472  uhgrspan1  29389  ip2i  30917  bcseqi  31209  hilnormi  31252  cmcmlem  31680  fh3i  31712  fh4i  31713  pjadjii  31763  resf1o  32821  dp3mul10  32975  dpmul4  32991  threehalves  32992  ressplusf  33041  cycpmconjs  33235  resvsca  33410  cos9thpiminplylem5  33949  xpinpreima  34069  cnre2csqima  34074  esum2dlem  34255  eulerpartgbij  34535  ballotth  34701  plymulx  34711  hgt750lem2  34815  elrn3  35963  itg2addnclem2  38010  dfsucmap3  38801  dfsucmap4  38803  dfcoss3  38842  cossid  38908  dfssr2  38917  dfpetparts2  39310  dfpeters2  39312  areaquad  43665  cnvrcl0  44073  stoweidlem13  46462  wallispi2  46522  fourierdlem96  46651  fourierdlem97  46652  fourierdlem98  46653  fourierdlem99  46654  fourierdlem113  46668  fourierswlem  46679  dfafv2  47595  dfnelbr2  47736  ceil5half3  47809  fmtnorec2  48021  fmtno5fac  48060  tposrescnv  49369  tposres3  49371  dfswapf2  49751  setrec2  50185