Theorem equcom 1754

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 1752	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1752	. 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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1755  sbal1yz  2057  dveeq1  2075  eu1  2107  reu7  3015  reu8  3016  dfdif3  3333  iunid  4052  copsexg  4365  opelopabsbALT  4382  dtruex  4686  opeliunxp  4810  relop  4910  dmi  4976  opabresid  5096  intirr  5154  cnvi  5172  coi1  5283  brprcneu  5668  f1oiso  6005  fvmpopr2d  6198  qsid  6847  mapsnend  7065  mapsnen  7066  suplocsrlem  8139  summodc  12094  bezoutlemle  12729  cnmptid  15272