Theorem eqtr2di 2255

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
eqtr2di.1	|- ( ph -> A = B )
eqtr2di.2	|- B = C

Assertion

Ref	Expression
eqtr2di	|- ( ph -> C = A )

Proof of Theorem eqtr2di

Step	Hyp	Ref	Expression
1		eqtr2di.1	. . 3 |- ( ph -> A = B )
2		eqtr2di.2	. . 3 |- B = C
3	1, 2	eqtrdi 2254	. 2 |- ( ph -> A = C )
4	3	eqcomd 2211	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = 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:  eqtr4id  2257  elxp4  5171  elxp5  5172  fo1stresm  6249  fo2ndresm  6250  eloprabi  6284  fo2ndf  6315  xpsnen  6918  xpassen  6927  ac6sfi  6997  undifdc  7023  ine0  8468  nn0n0n1ge2  9445  fzval2  10135  fseq1p1m1  10218  fsum2dlemstep  11778  modfsummodlemstep  11801  fprod2dlemstep  11966  ef4p  12038  sin01bnd  12101  odd2np1  12217  sqpweven  12530  2sqpwodd  12531  psmetdmdm  14829  xmetdmdm  14861  dveflem  15231  reeff1oleme  15277  abssinper  15351  lgseisenlem1  15580