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

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

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1633 . 2 (𝑥 = 𝑦𝑦 = 𝑥)
2 equcomi 1633 . 2 (𝑦 = 𝑥𝑥 = 𝑦)
31, 2impbii 124 1 (𝑥 = 𝑦𝑦 = 𝑥)
 Colors of variables: wff set class Syntax hints:   ↔ wb 103 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1379  ax-ie2 1424  ax-8 1436  ax-17 1460  ax-i9 1464 This theorem depends on definitions:  df-bi 115 This theorem is referenced by:  sbal1yz  1919  dveeq1  1937  eu1  1967  reu7  2788  reu8  2789  iunid  3741  copsexg  4007  opelopabsbALT  4022  dtruex  4310  opeliunxp  4421  relop  4514  dmi  4578  opabresid  4689  intirr  4741  cnvi  4758  coi1  4866  brprcneu  5202  f1oiso  5496  qsid  6237  bezoutlemle  10541
 Copyright terms: Public domain W3C validator