Theorem equcom 1729

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 1727	. 2 |- ( x = y -> y = x )
2		equcomi 1727	. 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 1472  ax-ie2 1517  ax-8 1527  ax-17 1549  ax-i9 1553

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1730  sbal1yz  2029  dveeq1  2047  eu1  2079  reu7  2968  reu8  2969  dfdif3  3283  iunid  3983  copsexg  4289  opelopabsbALT  4306  dtruex  4608  opeliunxp  4731  relop  4829  dmi  4894  opabresid  5013  intirr  5070  cnvi  5088  coi1  5199  brprcneu  5571  f1oiso  5897  fvmpopr2d  6084  qsid  6689  mapsnen  6905  suplocsrlem  7923  summodc  11727  bezoutlemle  12362  cnmptid  14786