Theorem 3eqtr4ri 2114

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

Syntax hints:   = wceq 1285

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-5 1377  ax-gen 1379  ax-4 1441  ax-17 1460  ax-ext 2065

This theorem depends on definitions:  df-bi 115  df-cleq 2076

This theorem is referenced by:  cbvreucsf  2976  dfif6  3371  qdass  3508  tpidm12  3510  unipr  3636  dfdm4  4576  dmun  4591  resres  4673  inres  4678  resiun1  4679  imainrect  4817  coundi  4873  coundir  4874  funopg  4985  offres  5815  mpt2mptsx  5876  cnvoprab  5908  snec  6256  halfpm6th  8395  numsucc  8674  decbin2  8775  znnen  10843