Theorem equcom 1730

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 1728	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1728	. 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 1473  ax-ie2 1518  ax-8 1528  ax-17 1550  ax-i9 1554

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1731  sbal1yz  2030  dveeq1  2048  eu1  2080  reu7  2972  reu8  2973  dfdif3  3287  iunid  3992  copsexg  4301  opelopabsbALT  4318  dtruex  4620  opeliunxp  4743  relop  4841  dmi  4907  opabresid  5026  intirr  5083  cnvi  5101  coi1  5212  brprcneu  5587  f1oiso  5913  fvmpopr2d  6100  qsid  6705  mapsnen  6922  suplocsrlem  7951  summodc  11779  bezoutlemle  12414  cnmptid  14838