Theorem equcomi 1750

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 1747	. 2 ⊢ 𝑥 = 𝑥
2		ax-8 1550	. 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 1495  ax-ie2 1540  ax-8 1550  ax-17 1572  ax-i9 1576

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax6evr  1751  equcom  1752  equcoms  1754  ax10  1763  cbv2h  1794  cbv2w  1796  equvini  1804  equveli  1805  equsb2  1832  drex1  1844  sbcof2  1856  aev  1858  cbvexdh  1973  rext  4300  iotaval  5289  prodmodc  12084