Theorem equcom 1758

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

This proof depends on syntax axioms:   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-gen 1502  ax-ie2 1547  ax-8 1557  ax-17 1579  ax-i9 1583

This proof depends on definitions:  df-bi 117

This theorem is used by:  equcomd  1759  sbal1yz  2061  dveeq1  2079  eu1  2111  reu7  3021  reu8  3022  dfdif3  3339  iunid  4068  copsexg  4386  opelopabsbALT  4403  dtruex  4708  opeliunxp  4832  relop  4932  dmi  4998  opabresid  5119  intirr  5177  cnvi  5195  coi1  5306  brprcneu  5691  f1oiso  6035  fvmpopr2d  6228  qsid  6878  mapsnend  7103  mapsnen  7104  suplocsrlem  8181  summodc  12175  bezoutlemle  12810  cnmptid  15507