Theorem eqtr2di 2227

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

Hypotheses

Ref	Expression
eqtr2di.1	⊢ (𝜑 → 𝐴 = 𝐵)
eqtr2di.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
eqtr2di	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem eqtr2di

Step	Hyp	Ref	Expression
1		eqtr2di.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		eqtr2di.2	. . 3 ⊢ 𝐵 = 𝐶
3	1, 2	eqtrdi 2226	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2183	1 ⊢ (𝜑 → 𝐶 = 𝐴)

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  5116  elxp5  5117  fo1stresm  6161  fo2ndresm  6162  eloprabi  6196  fo2ndf  6227  xpsnen  6820  xpassen  6829  ac6sfi  6897  undifdc  6922  ine0  8350  nn0n0n1ge2  9322  fzval2  10010  fseq1p1m1  10093  fsum2dlemstep  11441  modfsummodlemstep  11464  fprod2dlemstep  11629  ef4p  11701  sin01bnd  11764  odd2np1  11877  sqpweven  12174  2sqpwodd  12175  psmetdmdm  13794  xmetdmdm  13826  dveflem  14157  reeff1oleme  14163  abssinper  14237  lgseisenlem1  14420