Theorem 3eqtr4ri 2237

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

Syntax hints:   = wceq 1373

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 1470  ax-gen 1472  ax-4 1533  ax-17 1549  ax-ext 2187

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

This theorem is referenced by:  cbvreucsf  3158  dfif6  3573  qdass  3730  tpidm12  3732  unipr  3864  dfdm4  4870  dmun  4885  resres  4971  inres  4976  resdifcom  4977  resiun1  4978  imainrect  5128  coundi  5184  coundir  5185  funopg  5305  offres  6220  mpomptsx  6283  cnvoprab  6320  snec  6683  halfpm6th  9257  numsucc  9543  decbin2  9644  fsumadd  11717  fsum2d  11746  fprodmul  11902  fprodfac  11926  fprodrec  11940  znnen  12769  txswaphmeolem  14792