Theorem equcom 1717

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 1715	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1715	. 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 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1718  sbal1yz  2017  dveeq1  2035  eu1  2067  reu7  2956  reu8  2957  dfdif3  3270  iunid  3969  copsexg  4274  opelopabsbALT  4290  dtruex  4592  opeliunxp  4715  relop  4813  dmi  4878  opabresid  4996  intirr  5053  cnvi  5071  coi1  5182  brprcneu  5548  f1oiso  5870  fvmpopr2d  6056  qsid  6656  mapsnen  6867  suplocsrlem  7870  summodc  11529  bezoutlemle  12148  cnmptid  14460