Theorem equcomi 1728

Description: Commutative law for equality. Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.)

Assertion

Ref	Expression
equcomi	⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

Proof of Theorem equcomi

Step	Hyp	Ref	Expression
1		equid 1725	. 2 ⊢ 𝑥 = 𝑥
2		ax-8 1528	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 → 𝑦 = 𝑥))
3	1, 2	mpi 15	1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

Syntax hints:   → wi 4

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1473  ax-ie2 1518  ax-8 1528  ax-17 1550  ax-i9 1554

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax6evr  1729  equcom  1730  equcoms  1732  ax10  1741  cbv2h  1772  cbv2w  1774  equvini  1782  equveli  1783  equsb2  1810  drex1  1822  sbcof2  1834  aev  1836  cbvexdh  1951  rext  4267  iotaval  5252  prodmodc  11964