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  5118  elxp5  5119  fo1stresm  6164  fo2ndresm  6165  eloprabi  6199  fo2ndf  6230  xpsnen  6823  xpassen  6832  ac6sfi  6900  undifdc  6925  ine0  8353  nn0n0n1ge2  9325  fzval2  10013  fseq1p1m1  10096  fsum2dlemstep  11444  modfsummodlemstep  11467  fprod2dlemstep  11632  ef4p  11704  sin01bnd  11767  odd2np1  11880  sqpweven  12177  2sqpwodd  12178  psmetdmdm  13909  xmetdmdm  13941  dveflem  14272  reeff1oleme  14278  abssinper  14352  lgseisenlem1  14535