Theorem equcom 1706

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 1704	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1704	. 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 1449  ax-ie2 1494  ax-8 1504  ax-17 1526  ax-i9 1530

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1707  sbal1yz  2001  dveeq1  2019  eu1  2051  reu7  2934  reu8  2935  dfdif3  3247  iunid  3944  copsexg  4246  opelopabsbALT  4261  dtruex  4560  opeliunxp  4683  relop  4779  dmi  4844  opabresid  4962  intirr  5017  cnvi  5035  coi1  5146  brprcneu  5510  f1oiso  5829  qsid  6602  mapsnen  6813  suplocsrlem  7809  summodc  11393  bezoutlemle  12011  cnmptid  13820