ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  equcomi GIF version

Theorem equcomi 1681
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
StepHypRef Expression
1 equid 1678 . 2 𝑥 = 𝑥
2 ax-8 1483 . 2 (𝑥 = 𝑦 → (𝑥 = 𝑥𝑦 = 𝑥))
31, 2mpi 15 1 (𝑥 = 𝑦𝑦 = 𝑥)
Colors of variables: wff set class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-gen 1426  ax-ie2 1471  ax-8 1483  ax-17 1507  ax-i9 1511
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  ax6evr  1682  equcom  1683  equcoms  1685  ax10  1696  cbv2h  1725  equvini  1732  equveli  1733  equsb2  1760  drex1  1771  sbcof2  1783  aev  1785  cbvexdh  1899  rext  4144  iotaval  5106  prodmodc  11378
  Copyright terms: Public domain W3C validator