Theorem equcomi 1692

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 1689	. 2 ⊢ 𝑥 = 𝑥
2		ax-8 1492	. 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 105  ax-gen 1437  ax-ie2 1482  ax-8 1492  ax-17 1514  ax-i9 1518

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax6evr  1693  equcom  1694  equcoms  1696  ax10  1705  cbv2h  1736  cbv2w  1738  equvini  1746  equveli  1747  equsb2  1774  drex1  1786  sbcof2  1798  aev  1800  cbvexdh  1914  rext  4193  iotaval  5164  prodmodc  11519