Theorem equcom 1682

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 1680	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1680	. 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 1425  ax-ie2 1470  ax-8 1482  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equcomd  1683  sbal1yz  1974  dveeq1  1992  eu1  2022  reu7  2874  reu8  2875  dfdif3  3181  iunid  3863  copsexg  4161  opelopabsbALT  4176  dtruex  4469  opeliunxp  4589  relop  4684  dmi  4749  opabresid  4867  intirr  4920  cnvi  4938  coi1  5049  brprcneu  5407  f1oiso  5720  qsid  6487  mapsnen  6698  suplocsrlem  7609  summodc  11145  bezoutlemle  11685  cnmptid  12439