Theorem equcom 1720

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 1718	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1718	. 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 1463  ax-ie2 1508  ax-8 1518  ax-17 1540  ax-i9 1544

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1721  sbal1yz  2020  dveeq1  2038  eu1  2070  reu7  2959  reu8  2960  dfdif3  3273  iunid  3972  copsexg  4277  opelopabsbALT  4293  dtruex  4595  opeliunxp  4718  relop  4816  dmi  4881  opabresid  4999  intirr  5056  cnvi  5074  coi1  5185  brprcneu  5551  f1oiso  5873  fvmpopr2d  6059  qsid  6659  mapsnen  6870  suplocsrlem  7875  summodc  11548  bezoutlemle  12175  cnmptid  14517