Theorem 3eqtr2ri 2769

Description: An inference from three chained equalities. (Contributed by NM, 3-Aug-2006.) (Proof shortened by Andrew Salmon, 25-May-2011.)

Hypotheses

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

Assertion

Ref	Expression
3eqtr2ri	⊢ 𝐷 = 𝐴

Proof of Theorem 3eqtr2ri

Step	Hyp	Ref	Expression
1		3eqtr2i.1	. . 3 ⊢ 𝐴 = 𝐵
2		3eqtr2i.2	. . 3 ⊢ 𝐶 = 𝐵
3	1, 2	eqtr4i 2765	. 2 ⊢ 𝐴 = 𝐶
4		3eqtr2i.3	. 2 ⊢ 𝐶 = 𝐷
5	3, 4	eqtr2i 2763	1 ⊢ 𝐷 = 𝐴

Syntax hints:   = wceq 1547

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-ex 1787  df-cleq 2731

This theorem is referenced by:  funimacnv  6566  uniqs  8710  ackbij1lem13  10144  ef01bndlem  16142  cos2bnd  16146  divalglem2  16355  lefld  18549  smndex2dlinvh  18879  discmp  23381  unmbl  25522  sinhalfpilem  26445  log2cnv  26926  lgam1  27045  ip0i  30914  polid2i  31246  hh0v  31257  pjinormii  31765  dfdec100  32922  dpmul100  32975  dpmul  32991  dpmul4  32992  subfacp1lem3  35410  dmcnvep  38755  redvmptabs  42837  cotrclrcl  44186  sqwvfoura  46671  sqwvfourb  46672