Theorem 3eqtr4ri 2087

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

Syntax hints:   = wceq 1259

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-5 1352  ax-gen 1354  ax-4 1416  ax-17 1435  ax-ext 2038

This theorem depends on definitions:  df-bi 114  df-cleq 2049

This theorem is referenced by:  cbvreucsf  2937  dfif6  3360  qdass  3494  tpidm12  3496  unipr  3621  dfdm4  4554  dmun  4569  resres  4651  inres  4656  resiun1  4657  imainrect  4793  coundi  4849  coundir  4850  funopg  4961  offres  5789  mpt2mptsx  5850  cnvoprab  5882  snec  6197  halfpm6th  8201  numsucc  8465  decbin2  8566