Theorem equcom 1729

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 1727	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1727	. 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 1472  ax-ie2 1517  ax-8 1527  ax-17 1549  ax-i9 1553

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1730  sbal1yz  2029  dveeq1  2047  eu1  2079  reu7  2968  reu8  2969  dfdif3  3283  iunid  3983  copsexg  4288  opelopabsbALT  4305  dtruex  4607  opeliunxp  4730  relop  4828  dmi  4893  opabresid  5012  intirr  5069  cnvi  5087  coi1  5198  brprcneu  5569  f1oiso  5895  fvmpopr2d  6082  qsid  6687  mapsnen  6903  suplocsrlem  7921  summodc  11694  bezoutlemle  12329  cnmptid  14753