Theorem 3eqtr4ri 2261

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

Syntax hints:   = wceq 1395

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 1493  ax-gen 1495  ax-4 1556  ax-17 1572  ax-ext 2211

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

This theorem is referenced by:  cbvreucsf  3190  dfif6  3605  qdass  3766  tpidm12  3768  unipr  3905  dfdm4  4921  dmun  4936  resres  5023  inres  5028  resdifcom  5029  resiun1  5030  imainrect  5180  coundi  5236  coundir  5237  funopg  5358  offres  6292  mpomptsx  6357  cnvoprab  6394  snec  6760  halfpm6th  9354  numsucc  9640  decbin2  9741  fsumadd  11957  fsum2d  11986  fprodmul  12142  fprodfac  12166  fprodrec  12180  znnen  13009  txswaphmeolem  15034