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