Theorem eqtr2di 2288

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

This proof depends on syntax axioms:   -> wi 4   = wceq 1402

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-5 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

This proof depends on definitions:  df-bi 117  df-cleq 2231

This theorem is used by:  eqtr4id  2290  elpr2elpr  3901  elxp4  5278  elxp5  5279  fo1stresm  6399  fo2ndresm  6400  eloprabi  6436  fo2ndf  6467  xpsnen  7123  xpassen  7132  ac6sfi  7206  undifdc  7235  ine0  8728  nn0n0n1ge2  9726  fzval2  10431  fseq1p1m1  10518  hashfibclem  11304  hashf1  11309  fsum2dlemstep  12226  modfsummodlemstep  12249  fprod2dlemstep  12414  ef4p  12486  sin01bnd  12549  odd2np1  12665  sqpweven  12980  2sqpwodd  12981  psmetdmdm  15550  xmetdmdm  15582  dveflem  15952  reeff1oleme  15998  abssinper  16073  lgseisenlem1  16394