Theorem equcom 1680

Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.)

Assertion

Ref	Expression
equcom	⊢ (x = y ↔ y = x)

Proof of Theorem equcom

Step	Hyp	Ref	Expression
1		equcomi 1679	. 2 ⊢ (x = y → y = x)
2		equcomi 1679	. 2 ⊢ (y = x → x = y)
3	1, 2	impbii 180	1 ⊢ (x = y ↔ y = x)

Syntax hints:   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675

This theorem depends on definitions:  df-bi 177  df-ex 1542

This theorem is referenced by:  equequ2  1686  ax12olem6  1932  eu1  2225  2eu6  2289  reu8  3033  iunid  4022  unipw1  4326  addcid1  4406  evenodddisjlem1  4516  dfphi2  4570  proj1op  4601  proj2op  4602  copsexg  4608  phidisjnn  4616  dfid3  4769  opeliunxp  4821  dmi  4920  opabresid  5004  intirr  5030  cnvi  5033  coi1  5095  trtxp  5782  oqelins4  5795  fvfullfunlem1  5862  extex  5916  enpw1lem1  6062  el2c  6192  addccan2nclem1  6264  fnfreclem1  6318  scancan  6332