Theorem eqtr2di 2288

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 2287	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2244	1 ⊢ (𝜑 → 𝐶 = 𝐴)

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  5275  elxp5  5276  fo1stresm  6395  fo2ndresm  6396  eloprabi  6432  fo2ndf  6463  xpsnen  7119  xpassen  7128  ac6sfi  7202  undifdc  7231  ine0  8722  nn0n0n1ge2  9719  fzval2  10424  fseq1p1m1  10511  hashfibclem  11296  hashf1  11301  fsum2dlemstep  12217  modfsummodlemstep  12240  fprod2dlemstep  12405  ef4p  12477  sin01bnd  12540  odd2np1  12656  sqpweven  12971  2sqpwodd  12972  psmetdmdm  15474  xmetdmdm  15506  dveflem  15876  reeff1oleme  15922  abssinper  15997  lgseisenlem1  16287