Theorem equcomi 1715

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 1712	. 2 ⊢ 𝑥 = 𝑥
2		ax-8 1515	. 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 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax6evr  1716  equcom  1717  equcoms  1719  ax10  1728  cbv2h  1759  cbv2w  1761  equvini  1769  equveli  1770  equsb2  1797  drex1  1809  sbcof2  1821  aev  1823  cbvexdh  1938  rext  4233  iotaval  5207  prodmodc  11618