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

Theorem equcom 1566
 Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.)
Assertion
Ref Expression
equcom (x = yy = x)

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1565 . 2 (x = yy = x)
2 equcomi 1565 . 2 (y = xx = y)
31, 2impbii 117 1 (x = yy = x)
 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 1311  ax-ie2 1356  ax-8 1368  ax-17 1392  ax-i9 1396 This theorem depends on definitions:  df-bi 110 This theorem is referenced by:  sbal1yz  1850  dveeq1  1868  eu1  1898  reu7  2704  reu8  2705  iunid  3675  copsexg  3944  opelopabsbALT  3959  opeliunxp  4310  relop  4401  dmi  4465  opabresid  4574  intirr  4626  cnvi  4643  coi1  4751  brprcneu  5084  f1oiso  5378  qsid  6070
 Copyright terms: Public domain W3C validator