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

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

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1592 . 2 (𝑥 = 𝑦𝑦 = 𝑥)
2 equcomi 1592 . 2 (𝑦 = 𝑥𝑥 = 𝑦)
31, 2impbii 117 1 (𝑥 = 𝑦𝑦 = 𝑥)
Colors of variables: wff set class
Syntax hints:  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ie2 1383  ax-8 1395  ax-17 1419  ax-i9 1423
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  sbal1yz  1877  dveeq1  1895  eu1  1925  reu7  2736  reu8  2737  iunid  3712  copsexg  3981  opelopabsbALT  3996  opeliunxp  4395  relop  4486  dmi  4550  opabresid  4659  intirr  4711  cnvi  4728  coi1  4836  brprcneu  5171  f1oiso  5465  qsid  6171
  Copyright terms: Public domain W3C validator