Theorem eqtr2di 2254

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

Syntax hints:   → wi 4   = wceq 1372

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 1469  ax-gen 1471  ax-4 1532  ax-17 1548  ax-ext 2186

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

This theorem is referenced by:  eqtr4id  2256  elxp4  5169  elxp5  5170  fo1stresm  6246  fo2ndresm  6247  eloprabi  6281  fo2ndf  6312  xpsnen  6915  xpassen  6924  ac6sfi  6994  undifdc  7020  ine0  8465  nn0n0n1ge2  9442  fzval2  10132  fseq1p1m1  10215  fsum2dlemstep  11687  modfsummodlemstep  11710  fprod2dlemstep  11875  ef4p  11947  sin01bnd  12010  odd2np1  12126  sqpweven  12439  2sqpwodd  12440  psmetdmdm  14738  xmetdmdm  14770  dveflem  15140  reeff1oleme  15186  abssinper  15260  lgseisenlem1  15489