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 )

Syntax hints:   -> wi 4   = wceq 1402

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 1500  ax-gen 1502  ax-4 1563  ax-17 1579  ax-ext 2220

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

This theorem is referenced by:  eqtr4id  2290  elpr2elpr  3896  elxp4  5270  elxp5  5271  fo1stresm  6385  fo2ndresm  6386  eloprabi  6422  fo2ndf  6453  xpsnen  7109  xpassen  7118  ac6sfi  7192  undifdc  7221  ine0  8711  nn0n0n1ge2  9694  fzval2  10393  fseq1p1m1  10479  hashfibclem  11260  hashf1  11265  fsum2dlemstep  12179  modfsummodlemstep  12202  fprod2dlemstep  12367  ef4p  12439  sin01bnd  12502  odd2np1  12618  sqpweven  12931  2sqpwodd  12932  psmetdmdm  15348  xmetdmdm  15380  dveflem  15750  reeff1oleme  15796  abssinper  15870  lgseisenlem1  16103