Theorem equcom 1704

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 1702	. 2 |- ( x = y -> y = x )
2		equcomi 1702	. 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 1447  ax-ie2 1492  ax-8 1502  ax-17 1524  ax-i9 1528

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1705  sbal1yz  1999  dveeq1  2017  eu1  2049  reu7  2930  reu8  2931  dfdif3  3243  iunid  3937  copsexg  4238  opelopabsbALT  4253  dtruex  4552  opeliunxp  4675  relop  4770  dmi  4835  opabresid  4953  intirr  5007  cnvi  5025  coi1  5136  brprcneu  5500  f1oiso  5817  qsid  6590  mapsnen  6801  suplocsrlem  7782  summodc  11359  bezoutlemle  11976  cnmptid  13352