Theorem eqtr2di 2227

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

Syntax hints:   → wi 4   = wceq 1353

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 1447  ax-gen 1449  ax-4 1510  ax-17 1526  ax-ext 2159

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

This theorem is referenced by:  eqtr4id  2229  elxp4  5117  elxp5  5118  fo1stresm  6162  fo2ndresm  6163  eloprabi  6197  fo2ndf  6228  xpsnen  6821  xpassen  6830  ac6sfi  6898  undifdc  6923  ine0  8351  nn0n0n1ge2  9323  fzval2  10011  fseq1p1m1  10094  fsum2dlemstep  11442  modfsummodlemstep  11465  fprod2dlemstep  11630  ef4p  11702  sin01bnd  11765  odd2np1  11878  sqpweven  12175  2sqpwodd  12176  psmetdmdm  13827  xmetdmdm  13859  dveflem  14190  reeff1oleme  14196  abssinper  14270  lgseisenlem1  14453