Theorem equcom 1717

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 1715	. 2 ⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥)
2		equcomi 1715	. 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 1460  ax-ie2 1505  ax-8 1515  ax-17 1537  ax-i9 1541

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  equcomd  1718  sbal1yz  2017  dveeq1  2035  eu1  2067  reu7  2955  reu8  2956  dfdif3  3269  iunid  3968  copsexg  4273  opelopabsbALT  4289  dtruex  4591  opeliunxp  4714  relop  4812  dmi  4877  opabresid  4995  intirr  5052  cnvi  5070  coi1  5181  brprcneu  5547  f1oiso  5869  qsid  6654  mapsnen  6865  suplocsrlem  7868  summodc  11526  bezoutlemle  12145  cnmptid  14449