Theorem 3eqtr4ri 2236

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

Syntax hints:   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  cbvreucsf  3157  dfif6  3572  qdass  3729  tpidm12  3731  unipr  3863  dfdm4  4869  dmun  4884  resres  4970  inres  4975  resdifcom  4976  resiun1  4977  imainrect  5127  coundi  5183  coundir  5184  funopg  5304  offres  6219  mpomptsx  6282  cnvoprab  6319  snec  6682  halfpm6th  9256  numsucc  9542  decbin2  9643  fsumadd  11659  fsum2d  11688  fprodmul  11844  fprodfac  11868  fprodrec  11882  znnen  12711  txswaphmeolem  14734