Theorem equcom 1752

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 1750	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1750	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
3	1, 2	impbii 126	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

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 1495  ax-ie2 1540  ax-8 1550  ax-17 1572  ax-i9 1576

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1753  sbal1yz  2052  dveeq1  2070  eu1  2102  reu7  2998  reu8  2999  dfdif3  3314  iunid  4020  copsexg  4329  opelopabsbALT  4346  dtruex  4650  opeliunxp  4773  relop  4871  dmi  4937  opabresid  5057  intirr  5114  cnvi  5132  coi1  5243  brprcneu  5619  f1oiso  5949  fvmpopr2d  6140  qsid  6745  mapsnen  6962  suplocsrlem  7991  summodc  11889  bezoutlemle  12524  cnmptid  14949