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

Theorem equcomi 1715
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 1712 . 2 𝑥 = 𝑥
2 ax-8 1515 . 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 106  ax-gen 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  ax6evr  1716  equcom  1717  equcoms  1719  ax10  1728  cbv2h  1759  cbv2w  1761  equvini  1769  equveli  1770  equsb2  1797  drex1  1809  sbcof2  1821  aev  1823  cbvexdh  1938  rext  4233  iotaval  5207  prodmodc  11618
  Copyright terms: Public domain W3C validator