Theorem equcom 1686

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 1684	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1684	. 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 1429  ax-ie2 1474  ax-8 1484  ax-17 1506  ax-i9 1510

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equcomd  1687  sbal1yz  1981  dveeq1  1999  eu1  2031  reu7  2907  reu8  2908  dfdif3  3218  iunid  3906  copsexg  4207  opelopabsbALT  4222  dtruex  4521  opeliunxp  4644  relop  4739  dmi  4804  opabresid  4922  intirr  4975  cnvi  4993  coi1  5104  brprcneu  5464  f1oiso  5779  qsid  6548  mapsnen  6759  suplocsrlem  7731  summodc  11292  bezoutlemle  11908  cnmptid  12777