Theorem equcom 1699

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 1697	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1697	. 2 ⊢ (𝑦 = 𝑥 → 𝑥 = 𝑦)
3	1, 2	impbii 125	1 ⊢ (𝑥 = 𝑦 ↔ 𝑦 = 𝑥)

Syntax hints:   ↔ wb 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-gen 1442  ax-ie2 1487  ax-8 1497  ax-17 1519  ax-i9 1523

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  equcomd  1700  sbal1yz  1994  dveeq1  2012  eu1  2044  reu7  2925  reu8  2926  dfdif3  3237  iunid  3928  copsexg  4229  opelopabsbALT  4244  dtruex  4543  opeliunxp  4666  relop  4761  dmi  4826  opabresid  4944  intirr  4997  cnvi  5015  coi1  5126  brprcneu  5489  f1oiso  5805  qsid  6578  mapsnen  6789  suplocsrlem  7770  summodc  11346  bezoutlemle  11963  cnmptid  13075