Theorem 3eqtr4ri 2228

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

Syntax hints:   = wceq 1364

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 1461  ax-gen 1463  ax-4 1524  ax-17 1540  ax-ext 2178

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

This theorem is referenced by:  cbvreucsf  3149  dfif6  3564  qdass  3720  tpidm12  3722  unipr  3854  dfdm4  4859  dmun  4874  resres  4959  inres  4964  resdifcom  4965  resiun1  4966  imainrect  5116  coundi  5172  coundir  5173  funopg  5293  offres  6193  mpomptsx  6256  cnvoprab  6293  snec  6656  halfpm6th  9213  numsucc  9498  decbin2  9599  fsumadd  11573  fsum2d  11602  fprodmul  11758  fprodfac  11782  fprodrec  11796  znnen  12625  txswaphmeolem  14566