Theorem equcom 1693

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 1691	. 2 |- ( x = y -> y = x )
2		equcomi 1691	. 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 1436  ax-ie2 1481  ax-8 1491  ax-17 1513  ax-i9 1517

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equcomd  1694  sbal1yz  1988  dveeq1  2006  eu1  2038  reu7  2916  reu8  2917  dfdif3  3227  iunid  3915  copsexg  4216  opelopabsbALT  4231  dtruex  4530  opeliunxp  4653  relop  4748  dmi  4813  opabresid  4931  intirr  4984  cnvi  5002  coi1  5113  brprcneu  5473  f1oiso  5788  qsid  6557  mapsnen  6768  suplocsrlem  7740  summodc  11310  bezoutlemle  11926  cnmptid  12822