Theorem 3eqtr4ri 2119

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

Syntax hints:   = wceq 1289

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 1381  ax-gen 1383  ax-4 1445  ax-17 1464  ax-ext 2070

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

This theorem is referenced by:  cbvreucsf  2992  dfif6  3395  qdass  3539  tpidm12  3541  unipr  3667  dfdm4  4628  dmun  4643  resres  4725  inres  4730  resdifcom  4731  resiun1  4732  imainrect  4876  coundi  4932  coundir  4933  funopg  5048  offres  5906  mpt2mptsx  5967  cnvoprab  5999  snec  6351  halfpm6th  8634  numsucc  8914  decbin2  9015  fsumadd  10796  fsum2d  10825  znnen  11485