New Foundations Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  NFE Home  >  Th. List  >  equcom GIF version

Theorem equcom 1680
 Description: Commutative law for equality. (Contributed by NM, 20-Aug-1993.)
Assertion
Ref Expression
equcom (x = yy = x)

Proof of Theorem equcom
StepHypRef Expression
1 equcomi 1679 . 2 (x = yy = x)
2 equcomi 1679 . 2 (y = xx = y)
31, 2impbii 180 1 (x = yy = x)
 Colors of variables: wff setvar class Syntax hints:   ↔ wb 176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 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
 Copyright terms: Public domain W3C validator