Theorem eqtr2di 2204

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

Syntax hints:   → wi 4   = wceq 1332

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-5 1424  ax-gen 1426  ax-4 1487  ax-17 1503  ax-ext 2136

This theorem depends on definitions:  df-bi 116  df-cleq 2147

This theorem is referenced by:  eqtr4id  2206  elxp4  5066  elxp5  5067  fo1stresm  6099  fo2ndresm  6100  eloprabi  6134  fo2ndf  6164  xpsnen  6755  xpassen  6764  ac6sfi  6832  undifdc  6857  ine0  8248  nn0n0n1ge2  9213  fzval2  9893  fseq1p1m1  9974  fsum2dlemstep  11308  modfsummodlemstep  11331  fprod2dlemstep  11496  ef4p  11568  sin01bnd  11631  odd2np1  11737  sqpweven  12021  2sqpwodd  12022  psmetdmdm  12671  xmetdmdm  12703  dveflem  13034  reeff1oleme  13040  abssinper  13114