Theorem equcom 1752

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 1750	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1750	. 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 1495  ax-ie2 1540  ax-8 1550  ax-17 1572  ax-i9 1576

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1753  sbal1yz  2052  dveeq1  2070  eu1  2102  reu7  2998  reu8  2999  dfdif3  3314  iunid  4021  copsexg  4330  opelopabsbALT  4347  dtruex  4651  opeliunxp  4774  relop  4872  dmi  4938  opabresid  5058  intirr  5115  cnvi  5133  coi1  5244  brprcneu  5622  f1oiso  5956  fvmpopr2d  6147  qsid  6755  mapsnen  6972  suplocsrlem  8006  summodc  11909  bezoutlemle  12544  cnmptid  14970