Theorem equcomi 1756

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 1753	. 2 ⊢ 𝑥 = 𝑥
2		ax-8 1557	. 2 ⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 → 𝑦 = 𝑥))
3	1, 2	mpi 15	1 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)

This proof depends on syntax axioms:   → wi 4

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-gen 1502  ax-ie2 1547  ax-8 1557  ax-17 1579  ax-i9 1583

This proof depends on definitions:  df-bi 117

This theorem is used by:  ax6evr  1757  equcom  1758  equcoms  1760  ax10  1769  cbv2h  1801  cbv2w  1803  equvini  1811  equveli  1812  equsb2  1839  drex1  1851  sbcof2  1863  aev  1865  cbvexdh  1982  rext  4355  iotaval  5349  prodmodc  12345