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 1497  ax-ie2 1542  ax-8 1552  ax-17 1574  ax-i9 1578

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1755  sbal1yz  2054  dveeq1  2072  eu1  2104  reu7  3001  reu8  3002  dfdif3  3317  iunid  4026  copsexg  4336  opelopabsbALT  4353  dtruex  4657  opeliunxp  4781  relop  4880  dmi  4946  opabresid  5066  intirr  5123  cnvi  5141  coi1  5252  brprcneu  5632  f1oiso  5966  fvmpopr2d  6157  qsid  6768  mapsnen  6985  suplocsrlem  8027  summodc  11943  bezoutlemle  12578  cnmptid  15004