Theorem 3eqtr4ri 2238

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

Syntax hints:   = wceq 1373

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

This theorem depends on definitions:  df-bi 117  df-cleq 2199

This theorem is referenced by:  cbvreucsf  3162  dfif6  3577  qdass  3735  tpidm12  3737  unipr  3873  dfdm4  4884  dmun  4899  resres  4985  inres  4990  resdifcom  4991  resiun1  4992  imainrect  5142  coundi  5198  coundir  5199  funopg  5319  offres  6238  mpomptsx  6301  cnvoprab  6338  snec  6701  halfpm6th  9287  numsucc  9573  decbin2  9674  fsumadd  11802  fsum2d  11831  fprodmul  11987  fprodfac  12011  fprodrec  12025  znnen  12854  txswaphmeolem  14877