Theorem equcom 1717

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 1715	. 2 |- ( x = y -> y = x )
2		equcomi 1715	. 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 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1718  sbal1yz  2013  dveeq1  2031  eu1  2063  reu7  2947  reu8  2948  dfdif3  3260  iunid  3957  copsexg  4262  opelopabsbALT  4277  dtruex  4576  opeliunxp  4699  relop  4795  dmi  4860  opabresid  4978  intirr  5033  cnvi  5051  coi1  5162  brprcneu  5527  f1oiso  5848  qsid  6626  mapsnen  6837  suplocsrlem  7837  summodc  11423  bezoutlemle  12041  cnmptid  14238