Theorem equcomi 1691

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 1688	. 2 ⊢ 𝑥 = 𝑥
2		ax-8 1491	. 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 1436  ax-ie2 1481  ax-8 1491  ax-17 1513  ax-i9 1517

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  ax6evr  1692  equcom  1693  equcoms  1695  ax10  1704  cbv2h  1735  cbv2w  1737  equvini  1745  equveli  1746  equsb2  1773  drex1  1785  sbcof2  1797  aev  1799  cbvexdh  1913  rext  4187  iotaval  5158  prodmodc  11505