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  3032  iunid  4021  unipw1  4325  addcid1  4405  evenodddisjlem1  4515  dfphi2  4569  proj1op  4600  proj2op  4601  copsexg  4607  phidisjnn  4615  dfid3  4768  opeliunxp  4820  dmi  4919  opabresid  5003  intirr  5029  cnvi  5032  coi1  5094  trtxp  5781  oqelins4  5794  fvfullfunlem1  5861  extex  5915  enpw1lem1  6061  el2c  6191  addccan2nclem1  6263  fnfreclem1  6317  scancan  6331