Theorem equcomi 1752

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 1749	. 2 ⊢ 𝑥 = 𝑥
2		ax-8 1552	. 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 1497  ax-ie2 1542  ax-8 1552  ax-17 1574  ax-i9 1578

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ax6evr  1753  equcom  1754  equcoms  1756  ax10  1765  cbv2h  1796  cbv2w  1798  equvini  1806  equveli  1807  equsb2  1834  drex1  1846  sbcof2  1858  aev  1860  cbvexdh  1975  rext  4307  iotaval  5298  prodmodc  12138