Theorem equcomi 1697

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 1694	. 2 ⊢ 𝑥 = 𝑥
2		ax-8 1497	. 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 105  ax-gen 1442  ax-ie2 1487  ax-8 1497  ax-17 1519  ax-i9 1523

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax6evr  1698  equcom  1699  equcoms  1701  ax10  1710  cbv2h  1741  cbv2w  1743  equvini  1751  equveli  1752  equsb2  1779  drex1  1791  sbcof2  1803  aev  1805  cbvexdh  1919  rext  4200  iotaval  5171  prodmodc  11541