Theorem equcomi 1726

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 1723	. 2 ⊢ 𝑥 = 𝑥
2		ax-8 1526	. 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 1471  ax-ie2 1516  ax-8 1526  ax-17 1548  ax-i9 1552

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax6evr  1727  equcom  1728  equcoms  1730  ax10  1739  cbv2h  1770  cbv2w  1772  equvini  1780  equveli  1781  equsb2  1808  drex1  1820  sbcof2  1832  aev  1834  cbvexdh  1949  rext  4258  iotaval  5242  prodmodc  11831