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

Theorem equcom 1686
Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.)
Assertion
Ref Expression
equcom (𝑥 = 𝑦𝑦 = 𝑥)

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1684 . 2 (𝑥 = 𝑦𝑦 = 𝑥)
2 equcomi 1684 . 2 (𝑦 = 𝑥𝑥 = 𝑦)
31, 2impbii 125 1 (𝑥 = 𝑦𝑦 = 𝑥)
Colors of variables: wff set class
Syntax hints:  wb 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1429  ax-ie2 1474  ax-8 1484  ax-17 1506  ax-i9 1510
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  equcomd  1687  sbal1yz  1981  dveeq1  1999  eu1  2031  reu7  2907  reu8  2908  dfdif3  3218  iunid  3906  copsexg  4207  opelopabsbALT  4222  dtruex  4521  opeliunxp  4644  relop  4739  dmi  4804  opabresid  4922  intirr  4975  cnvi  4993  coi1  5104  brprcneu  5464  f1oiso  5779  qsid  6548  mapsnen  6759  suplocsrlem  7731  summodc  11292  bezoutlemle  11908  cnmptid  12777
  Copyright terms: Public domain W3C validator