Theorem equcomi 1718

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 1715	. 2 ⊢ 𝑥 = 𝑥
2		ax-8 1518	. 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 1463  ax-ie2 1508  ax-8 1518  ax-17 1540  ax-i9 1544

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax6evr  1719  equcom  1720  equcoms  1722  ax10  1731  cbv2h  1762  cbv2w  1764  equvini  1772  equveli  1773  equsb2  1800  drex1  1812  sbcof2  1824  aev  1826  cbvexdh  1941  rext  4248  iotaval  5230  prodmodc  11743