Theorem equcom 1694

Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.)

Assertion

Ref	Expression
equcom	⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Proof of Theorem equcom

Step	Hyp	Ref	Expression
1		equcomi 1692	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1692	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
3	1, 2	impbii 125	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1437  ax-ie2 1482  ax-8 1492  ax-17 1514  ax-i9 1518

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equcomd  1695  sbal1yz  1989  dveeq1  2007  eu1  2039  reu7  2921  reu8  2922  dfdif3  3232  iunid  3921  copsexg  4222  opelopabsbALT  4237  dtruex  4536  opeliunxp  4659  relop  4754  dmi  4819  opabresid  4937  intirr  4990  cnvi  5008  coi1  5119  brprcneu  5479  f1oiso  5794  qsid  6566  mapsnen  6777  suplocsrlem  7749  summodc  11324  bezoutlemle  11941  cnmptid  12921