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

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

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1637 . 2 (𝑥 = 𝑦𝑦 = 𝑥)
2 equcomi 1637 . 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 1383  ax-ie2 1428  ax-8 1440  ax-17 1464  ax-i9 1468
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  equcomd  1640  sbal1yz  1925  dveeq1  1943  eu1  1973  reu7  2808  reu8  2809  dfdif3  3108  iunid  3780  copsexg  4062  opelopabsbALT  4077  dtruex  4365  opeliunxp  4481  relop  4574  dmi  4639  opabresid  4752  intirr  4805  cnvi  4823  coi1  4933  brprcneu  5282  f1oiso  5587  qsid  6337  mapsnen  6508  isummo  10737  bezoutlemle  11079
  Copyright terms: Public domain W3C validator