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

Theorem equcom 1650
Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.)
Assertion
Ref Expression
equcom  |-  ( x  =  y  <->  y  =  x )

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1648 . 2  |-  ( x  =  y  ->  y  =  x )
2 equcomi 1648 . 2  |-  ( y  =  x  ->  x  =  y )
31, 2impbii 125 1  |-  ( x  =  y  <->  y  =  x )
Colors of variables: wff set class
Syntax hints:    <-> wb 104
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1393  ax-ie2 1438  ax-8 1450  ax-17 1474  ax-i9 1478
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  equcomd  1651  sbal1yz  1937  dveeq1  1955  eu1  1985  reu7  2832  reu8  2833  dfdif3  3133  iunid  3815  copsexg  4104  opelopabsbALT  4119  dtruex  4412  opeliunxp  4532  relop  4627  dmi  4692  opabresid  4808  intirr  4861  cnvi  4879  coi1  4990  brprcneu  5346  f1oiso  5659  qsid  6424  mapsnen  6635  summodc  10991  bezoutlemle  11489  cnmptid  12231
  Copyright terms: Public domain W3C validator