Theorem eqtr2di 2243

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

Syntax hints:   → wi 4   = wceq 1364

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 1458  ax-gen 1460  ax-4 1521  ax-17 1537  ax-ext 2175

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

This theorem is referenced by:  eqtr4id  2245  elxp4  5153  elxp5  5154  fo1stresm  6214  fo2ndresm  6215  eloprabi  6249  fo2ndf  6280  xpsnen  6875  xpassen  6884  ac6sfi  6954  undifdc  6980  ine0  8413  nn0n0n1ge2  9387  fzval2  10077  fseq1p1m1  10160  fsum2dlemstep  11577  modfsummodlemstep  11600  fprod2dlemstep  11765  ef4p  11837  sin01bnd  11900  odd2np1  12014  sqpweven  12313  2sqpwodd  12314  psmetdmdm  14492  xmetdmdm  14524  dveflem  14872  reeff1oleme  14907  abssinper  14981  lgseisenlem1  15186