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 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

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 1502  ax-ie2 1547  ax-8 1557  ax-17 1579  ax-i9 1583

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1759  sbal1yz  2061  dveeq1  2079  eu1  2111  reu7  3021  reu8  3022  dfdif3  3339  iunid  4063  copsexg  4379  opelopabsbALT  4396  dtruex  4701  opeliunxp  4825  relop  4925  dmi  4991  opabresid  5111  intirr  5169  cnvi  5187  coi1  5298  brprcneu  5683  f1oiso  6022  fvmpopr2d  6215  qsid  6864  mapsnend  7089  mapsnen  7090  suplocsrlem  8165  summodc  12128  bezoutlemle  12763  cnmptid  15305