Theorem eqtr2di 2227

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 2226	. 2 |- ( ph -> A = C )
4	3	eqcomd 2183	1 |- ( ph -> C = A )

Syntax hints:   -> wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqtr4id  2229  elxp4  5114  elxp5  5115  fo1stresm  6158  fo2ndresm  6159  eloprabi  6193  fo2ndf  6224  xpsnen  6817  xpassen  6826  ac6sfi  6894  undifdc  6919  ine0  8346  nn0n0n1ge2  9318  fzval2  10006  fseq1p1m1  10088  fsum2dlemstep  11434  modfsummodlemstep  11457  fprod2dlemstep  11622  ef4p  11694  sin01bnd  11757  odd2np1  11869  sqpweven  12166  2sqpwodd  12167  psmetdmdm  13686  xmetdmdm  13718  dveflem  14049  reeff1oleme  14055  abssinper  14129