ILE Home 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