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

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

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1663 . 2 (𝑥 = 𝑦𝑦 = 𝑥)
2 equcomi 1663 . 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 1408  ax-ie2 1453  ax-8 1465  ax-17 1489  ax-i9 1493 This theorem depends on definitions:  df-bi 116 This theorem is referenced by:  equcomd  1666  sbal1yz  1952  dveeq1  1970  eu1  2000  reu7  2850  reu8  2851  dfdif3  3154  iunid  3836  copsexg  4134  opelopabsbALT  4149  dtruex  4442  opeliunxp  4562  relop  4657  dmi  4722  opabresid  4840  intirr  4893  cnvi  4911  coi1  5022  brprcneu  5380  f1oiso  5693  qsid  6460  mapsnen  6671  suplocsrlem  7580  summodc  11092  bezoutlemle  11592  cnmptid  12345
 Copyright terms: Public domain W3C validator