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

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
StepHypRef Expression
1 equid 1694 . 2 𝑥 = 𝑥
2 ax-8 1497 . 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 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  4198  iotaval  5169  prodmodc  11528
  Copyright terms: Public domain W3C validator