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  2057  dveeq1  2075  eu1  2107  reu7  3014  reu8  3015  dfdif3  3331  iunid  4049  copsexg  4362  opelopabsbALT  4379  dtruex  4683  opeliunxp  4807  relop  4907  dmi  4973  opabresid  5093  intirr  5151  cnvi  5169  coi1  5280  brprcneu  5665  f1oiso  6001  fvmpopr2d  6192  qsid  6836  mapsnend  7054  mapsnen  7055  suplocsrlem  8125  summodc  12073  bezoutlemle  12708  cnmptid  15163