Theorem 3eqtr4ri 2266

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

Syntax hints:   = wceq 1398

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 1496  ax-gen 1498  ax-4 1559  ax-17 1575  ax-ext 2216

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

This theorem is referenced by:  cbvreucsf  3206  dfif6  3626  qdass  3793  tpidm12  3795  unipr  3933  dfdm4  4953  dmun  4968  resres  5055  inres  5060  resdifcom  5061  resiun1  5062  imainrect  5213  coundi  5269  coundir  5270  funopg  5391  offres  6341  mpomptsx  6406  cnvoprab  6443  snec  6843  halfpm6th  9475  numsucc  9766  decbin2  9867  fsumadd  12117  fsum2d  12146  fprodmul  12302  fprodfac  12326  fprodrec  12340  ballotfilemth  13225  znnen  13233  txswaphmeolem  15311