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

Step	Hyp	Ref	Expression
1		equcomi 1648	. 2 |- ( x = y -> y = x )
2		equcomi 1648	. 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-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