Theorem equcom 1706

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 1704	. 2 |- ( x = y -> y = x )
2		equcomi 1704	. 2 |- ( y = x -> x = y )
3	1, 2	impbii 126	1 |- ( x = y <-> y = x )

Syntax hints:   <-> wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1707  sbal1yz  2001  dveeq1  2019  eu1  2051  reu7  2933  reu8  2934  dfdif3  3246  iunid  3943  copsexg  4245  opelopabsbALT  4260  dtruex  4559  opeliunxp  4682  relop  4778  dmi  4843  opabresid  4961  intirr  5016  cnvi  5034  coi1  5145  brprcneu  5509  f1oiso  5827  qsid  6600  mapsnen  6811  suplocsrlem  7807  summodc  11391  bezoutlemle  12009  cnmptid  13784