Theorem equcom 1730

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 1728	. 2 |- ( x = y -> y = x )
2		equcomi 1728	. 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 1473  ax-ie2 1518  ax-8 1528  ax-17 1550  ax-i9 1554

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1731  sbal1yz  2030  dveeq1  2048  eu1  2080  reu7  2975  reu8  2976  dfdif3  3291  iunid  3997  copsexg  4306  opelopabsbALT  4323  dtruex  4625  opeliunxp  4748  relop  4846  dmi  4912  opabresid  5031  intirr  5088  cnvi  5106  coi1  5217  brprcneu  5592  f1oiso  5918  fvmpopr2d  6105  qsid  6710  mapsnen  6927  suplocsrlem  7956  summodc  11809  bezoutlemle  12444  cnmptid  14868