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 1498  ax-ie2 1543  ax-8 1553  ax-17 1575  ax-i9 1579

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1755  sbal1yz  2054  dveeq1  2072  eu1  2104  reu7  3002  reu8  3003  dfdif3  3319  iunid  4031  copsexg  4342  opelopabsbALT  4359  dtruex  4663  opeliunxp  4787  relop  4886  dmi  4952  opabresid  5072  intirr  5130  cnvi  5148  coi1  5259  brprcneu  5641  f1oiso  5977  fvmpopr2d  6168  qsid  6812  mapsnen  7029  suplocsrlem  8071  summodc  12007  bezoutlemle  12642  cnmptid  15075