Theorem 3eqtr3ri 2797

Description: An inference from three chained equalities. (Contributed by NM, 15-Aug-2004.)

Hypotheses

Ref	Expression
3eqtr3i.1	⊢ 𝐴 = 𝐵
3eqtr3i.2	⊢ 𝐴 = 𝐶
3eqtr3i.3	⊢ 𝐵 = 𝐷

Assertion

Ref	Expression
3eqtr3ri	⊢ 𝐷 = 𝐶

Proof of Theorem 3eqtr3ri

Step	Hyp	Ref	Expression
1		3eqtr3i.3	. 2 ⊢ 𝐵 = 𝐷
2		3eqtr3i.1	. . 3 ⊢ 𝐴 = 𝐵
3		3eqtr3i.2	. . 3 ⊢ 𝐴 = 𝐶
4	2, 3	eqtr3i 2790	. 2 ⊢ 𝐵 = 𝐶
5	1, 4	eqtr3i 2790	1 ⊢ 𝐷 = 𝐶

This proof depends on syntax axioms:   = wceq 1570

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-ex 1813  df-cleq 2757

This theorem is used by:  indif2  4234  dfif5  4506  resindm  6031  resdm2  6234  co01  6265  funiunfv  7251  dfdom2  8981  crreczi  14282  rei  15231  bpoly3  16134  bpoly4  16135  cos1bnd  16265  rpnnen2lem3  16294  rpnnen2lem11  16302  m1bits  16520  6gcd4e2  16618  3lcm2e6  16813  karatsuba  17165  ring1  20439  sincos4thpi  26729  sincos6thpi  26732  1cubrlem  27057  cht3  27388  bclbnd  27495  bposlem8  27506  ex-ind-dvds  30883  ip1ilem  31249  mdexchi  32758  disjxpin  33004  xppreima  33061  df1stres  33120  df2ndres  33121  dpmul100  33286  0dp2dp  33298  dpmul  33302  dpmul4  33303  xrge0slmod  33732  cos9thpiminplylem5  34240  cnrrext  34464  ballotth  34993  hgt750lemd  35100  poimirlem3  38331  poimirlem30  38358  mbfposadd  38375  asindmre  38411  refrelsredund4  39423  420gcd8e4  42831  sqmid3api  43102  areaquad  44001  inductionexd  44939  stoweidlem26  46798  3exp4mod41  48426  tposresg  49713