Theorem equcom 1754

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 1752	. 2 |- ( x = y -> y = x )
2		equcomi 1752	. 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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1755  sbal1yz  2055  dveeq1  2073  eu1  2105  reu7  3012  reu8  3013  dfdif3  3329  iunid  4047  copsexg  4360  opelopabsbALT  4377  dtruex  4681  opeliunxp  4805  relop  4905  dmi  4971  opabresid  5091  intirr  5149  cnvi  5167  coi1  5278  brprcneu  5663  f1oiso  5999  fvmpopr2d  6190  qsid  6834  mapsnend  7052  mapsnen  7053  suplocsrlem  8123  summodc  12069  bezoutlemle  12704  cnmptid  15146