Theorem eqtr2di 2256

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

Syntax hints:   → wi 4   = wceq 1373

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 1471  ax-gen 1473  ax-4 1534  ax-17 1550  ax-ext 2188

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

This theorem is referenced by:  eqtr4id  2258  elxp4  5179  elxp5  5180  fo1stresm  6260  fo2ndresm  6261  eloprabi  6295  fo2ndf  6326  xpsnen  6931  xpassen  6940  ac6sfi  7010  undifdc  7036  ine0  8486  nn0n0n1ge2  9463  fzval2  10153  fseq1p1m1  10236  fsum2dlemstep  11820  modfsummodlemstep  11843  fprod2dlemstep  12008  ef4p  12080  sin01bnd  12143  odd2np1  12259  sqpweven  12572  2sqpwodd  12573  psmetdmdm  14871  xmetdmdm  14903  dveflem  15273  reeff1oleme  15319  abssinper  15393  lgseisenlem1  15622