Theorem equcom 1728

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 1726	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1726	. 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 1471  ax-ie2 1516  ax-8 1526  ax-17 1548  ax-i9 1552

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1729  sbal1yz  2028  dveeq1  2046  eu1  2078  reu7  2967  reu8  2968  dfdif3  3282  iunid  3982  copsexg  4287  opelopabsbALT  4304  dtruex  4606  opeliunxp  4729  relop  4827  dmi  4892  opabresid  5011  intirr  5068  cnvi  5086  coi1  5197  brprcneu  5568  f1oiso  5894  fvmpopr2d  6081  qsid  6686  mapsnen  6902  suplocsrlem  7920  summodc  11665  bezoutlemle  12300  cnmptid  14724