Theorem 3eqtr4ri 2172

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

Syntax hints:   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1488  ax-17 1507  ax-ext 2122

This theorem depends on definitions:  df-bi 116  df-cleq 2133

This theorem is referenced by:  cbvreucsf  3069  dfif6  3481  qdass  3628  tpidm12  3630  unipr  3758  dfdm4  4739  dmun  4754  resres  4839  inres  4844  resdifcom  4845  resiun1  4846  imainrect  4992  coundi  5048  coundir  5049  funopg  5165  offres  6041  mpomptsx  6103  cnvoprab  6139  snec  6498  halfpm6th  8964  numsucc  9245  decbin2  9346  fsumadd  11207  fsum2d  11236  znnen  11947