Theorem equcom 1633

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

Syntax hints:   <-> wb 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-gen 1378  ax-ie2 1423  ax-8 1435  ax-17 1459  ax-i9 1463

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  sbal1yz  1918  dveeq1  1936  eu1  1966  reu7  2787  reu8  2788  iunid  3733  copsexg  3999  opelopabsbALT  4014  dtruex  4302  opeliunxp  4413  relop  4504  dmi  4568  opabresid  4679  intirr  4731  cnvi  4748  coi1  4856  brprcneu  5191  f1oiso  5485  qsid  6194  bezoutlemle  10397