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  2999  reu8  3000  dfdif3  3315  iunid  4024  copsexg  4334  opelopabsbALT  4351  dtruex  4655  opeliunxp  4779  relop  4878  dmi  4944  opabresid  5064  intirr  5121  cnvi  5139  coi1  5250  brprcneu  5628  f1oiso  5962  fvmpopr2d  6153  qsid  6764  mapsnen  6981  suplocsrlem  8018  summodc  11934  bezoutlemle  12569  cnmptid  14995