Theorem 3eqtr4ri 2225

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	|- A = B
3eqtr4i.2	|- C = A
3eqtr4i.3	|- D = B

Assertion

Ref	Expression
3eqtr4ri	|- D = C

Proof of Theorem 3eqtr4ri

Step	Hyp	Ref	Expression
1		3eqtr4i.3	. . 3 |- D = B
2		3eqtr4i.1	. . 3 |- A = B
3	1, 2	eqtr4i 2217	. 2 |- D = A
4		3eqtr4i.2	. 2 |- C = A
5	3, 4	eqtr4i 2217	1 |- D = C

Syntax hints:   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  cbvreucsf  3146  dfif6  3560  qdass  3716  tpidm12  3718  unipr  3850  dfdm4  4855  dmun  4870  resres  4955  inres  4960  resdifcom  4961  resiun1  4962  imainrect  5112  coundi  5168  coundir  5169  funopg  5289  offres  6189  mpomptsx  6252  cnvoprab  6289  snec  6652  halfpm6th  9205  numsucc  9490  decbin2  9591  fsumadd  11552  fsum2d  11581  fprodmul  11737  fprodfac  11761  fprodrec  11775  znnen  12558  txswaphmeolem  14499