Theorem 3eqtr4ri 2202

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

Syntax hints:   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  cbvreucsf  3113  dfif6  3527  qdass  3678  tpidm12  3680  unipr  3808  dfdm4  4801  dmun  4816  resres  4901  inres  4906  resdifcom  4907  resiun1  4908  imainrect  5054  coundi  5110  coundir  5111  funopg  5230  offres  6111  mpomptsx  6173  cnvoprab  6210  snec  6570  halfpm6th  9085  numsucc  9369  decbin2  9470  fsumadd  11356  fsum2d  11385  fprodmul  11541  fprodfac  11565  fprodrec  11579  znnen  12340