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  3274  iunid  3973  copsexg  4278  opelopabsbALT  4294  dtruex  4596  opeliunxp  4719  relop  4817  dmi  4882  opabresid  5000  intirr  5057  cnvi  5075  coi1  5186  brprcneu  5552  f1oiso  5874  fvmpopr2d  6061  qsid  6661  mapsnen  6872  suplocsrlem  7878  summodc  11551  bezoutlemle  12186  cnmptid  14543