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  5167  elxp5  5168  fo1stresm  6237  fo2ndresm  6238  eloprabi  6272  fo2ndf  6303  xpsnen  6898  xpassen  6907  ac6sfi  6977  undifdc  7003  ine0  8448  nn0n0n1ge2  9425  fzval2  10115  fseq1p1m1  10198  fsum2dlemstep  11664  modfsummodlemstep  11687  fprod2dlemstep  11852  ef4p  11924  sin01bnd  11987  odd2np1  12103  sqpweven  12416  2sqpwodd  12417  psmetdmdm  14714  xmetdmdm  14746  dveflem  15116  reeff1oleme  15162  abssinper  15236  lgseisenlem1  15465