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  4384  opelopabsbALT  4401  dtruex  4706  opeliunxp  4830  relop  4930  dmi  4996  opabresid  5116  intirr  5174  cnvi  5192  coi1  5303  brprcneu  5688  f1oiso  6032  fvmpopr2d  6225  qsid  6874  mapsnend  7099  mapsnen  7100  suplocsrlem  8175  summodc  12150  bezoutlemle  12785  cnmptid  15382