Theorem equcom 1683

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 1681	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1681	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
3	1, 2	impbii 125	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1426  ax-ie2 1471  ax-8 1483  ax-17 1507  ax-i9 1511

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equcomd  1684  sbal1yz  1977  dveeq1  1995  eu1  2025  reu7  2883  reu8  2884  dfdif3  3191  iunid  3876  copsexg  4174  opelopabsbALT  4189  dtruex  4482  opeliunxp  4602  relop  4697  dmi  4762  opabresid  4880  intirr  4933  cnvi  4951  coi1  5062  brprcneu  5422  f1oiso  5735  qsid  6502  mapsnen  6713  suplocsrlem  7640  summodc  11184  bezoutlemle  11732  cnmptid  12489