Theorem 3eqtr2ri 2767

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

Syntax hints:   = wceq 1542

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-ex 1782  df-cleq 2729

This theorem is referenced by:  funimacnv  6574  uniqs  8714  ackbij1lem13  10147  ef01bndlem  16145  cos2bnd  16149  divalglem2  16358  lefld  18552  smndex2dlinvh  18882  discmp  23376  unmbl  25517  sinhalfpilem  26443  log2cnv  26924  lgam1  27044  ip0i  30914  polid2i  31246  hh0v  31257  pjinormii  31765  dfdec100  32921  dpmul100  32974  dpmul  32990  dpmul4  32991  subfacp1lem3  35383  dmcnvep  38726  redvmptabs  42809  cotrclrcl  44190  sqwvfoura  46677  sqwvfourb  46678