Theorem syl6req 2189

Description: An equality transitivity deduction. (Contributed by NM, 29-Mar-1998.)

Hypotheses

Ref	Expression
syl6req.1	⊢ (𝜑 → 𝐴 = 𝐵)
syl6req.2	⊢ 𝐵 = 𝐶

Assertion

Ref	Expression
syl6req	⊢ (𝜑 → 𝐶 = 𝐴)

Proof of Theorem syl6req

Step	Hyp	Ref	Expression
1		syl6req.1	. . 3 ⊢ (𝜑 → 𝐴 = 𝐵)
2		syl6req.2	. . 3 ⊢ 𝐵 = 𝐶
3	1, 2	syl6eq 2188	. 2 ⊢ (𝜑 → 𝐴 = 𝐶)
4	3	eqcomd 2145	1 ⊢ (𝜑 → 𝐶 = 𝐴)

Syntax hints:   → wi 4   = wceq 1331

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 1423  ax-gen 1425  ax-4 1487  ax-17 1506  ax-ext 2121

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

This theorem is referenced by:  syl6reqr  2191  elxp4  5026  elxp5  5027  fo1stresm  6059  fo2ndresm  6060  eloprabi  6094  fo2ndf  6124  xpsnen  6715  xpassen  6724  ac6sfi  6792  undifdc  6812  ine0  8156  nn0n0n1ge2  9121  fzval2  9793  fseq1p1m1  9874  fsum2dlemstep  11203  modfsummodlemstep  11226  ef4p  11400  sin01bnd  11464  odd2np1  11570  sqpweven  11853  2sqpwodd  11854  psmetdmdm  12493  xmetdmdm  12525  dveflem  12855  abssinper  12927