Theorem equcom 1682

Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.)

Assertion

Ref	Expression
equcom	|- ( x = y <-> y = x )

Proof of Theorem equcom

Step	Hyp	Ref	Expression
1		equcomi 1680	. 2 |- ( x = y -> y = x )
2		equcomi 1680	. 2 |- ( y = x -> x = y )
3	1, 2	impbii 125	1 |- ( x = y <-> y = x )

Syntax hints:   <-> wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1425  ax-ie2 1470  ax-8 1482  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equcomd  1683  sbal1yz  1976  dveeq1  1994  eu1  2024  reu7  2879  reu8  2880  dfdif3  3186  iunid  3868  copsexg  4166  opelopabsbALT  4181  dtruex  4474  opeliunxp  4594  relop  4689  dmi  4754  opabresid  4872  intirr  4925  cnvi  4943  coi1  5054  brprcneu  5414  f1oiso  5727  qsid  6494  mapsnen  6705  suplocsrlem  7616  summodc  11152  bezoutlemle  11696  cnmptid  12450