Theorem equcom 1593

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 1592	. 2 |- ( x = y -> y = x )
2		equcomi 1592	. 2 |- ( y = x -> x = y )
3	1, 2	impbii 117	1 |- ( x = y <-> y = x )

Syntax hints:   <-> wb 98

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-gen 1338  ax-ie2 1383  ax-8 1395  ax-17 1419  ax-i9 1423

This theorem depends on definitions:  df-bi 110

This theorem is referenced by:  sbal1yz  1877  dveeq1  1895  eu1  1925  reu7  2736  reu8  2737  iunid  3712  copsexg  3981  opelopabsbALT  3996  opeliunxp  4395  relop  4486  dmi  4550  opabresid  4659  intirr  4711  cnvi  4728  coi1  4836  brprcneu  5171  f1oiso  5465  qsid  6171