Theorem eqtr2di 2216

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

Syntax hints:   → wi 4   = wceq 1343

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 1435  ax-gen 1437  ax-4 1498  ax-17 1514  ax-ext 2147

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

This theorem is referenced by:  eqtr4id  2218  elxp4  5091  elxp5  5092  fo1stresm  6129  fo2ndresm  6130  eloprabi  6164  fo2ndf  6195  xpsnen  6787  xpassen  6796  ac6sfi  6864  undifdc  6889  ine0  8292  nn0n0n1ge2  9261  fzval2  9947  fseq1p1m1  10029  fsum2dlemstep  11375  modfsummodlemstep  11398  fprod2dlemstep  11563  ef4p  11635  sin01bnd  11698  odd2np1  11810  sqpweven  12107  2sqpwodd  12108  psmetdmdm  12964  xmetdmdm  12996  dveflem  13327  reeff1oleme  13333  abssinper  13407