Theorem eqtr2di 2220

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

Syntax hints:   → wi 4   = wceq 1348

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 1440  ax-gen 1442  ax-4 1503  ax-17 1519  ax-ext 2152

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

This theorem is referenced by:  eqtr4id  2222  elxp4  5098  elxp5  5099  fo1stresm  6140  fo2ndresm  6141  eloprabi  6175  fo2ndf  6206  xpsnen  6799  xpassen  6808  ac6sfi  6876  undifdc  6901  ine0  8313  nn0n0n1ge2  9282  fzval2  9968  fseq1p1m1  10050  fsum2dlemstep  11397  modfsummodlemstep  11420  fprod2dlemstep  11585  ef4p  11657  sin01bnd  11720  odd2np1  11832  sqpweven  12129  2sqpwodd  12130  psmetdmdm  13118  xmetdmdm  13150  dveflem  13481  reeff1oleme  13487  abssinper  13561