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

Theorem equcomi 1679
Description: Commutative law for equality. Lemma 3 of [KalishMontague] p. 85. See also Lemma 7 of [Tarski] p. 69. (Contributed by NM, 5-Aug-1993.) (Revised by NM, 9-Apr-2017.)
Assertion
Ref Expression
equcomi (x = yy = x)

Proof of Theorem equcomi
StepHypRef Expression
1 equid 1676 . 2 x = x
2 ax-8 1675 . 2 (x = y → (x = xy = x))
31, 2mpi 16 1 (x = yy = x)
Colors of variables: wff setvar class
Syntax hints:  wi 4
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:  equcom  1680  equcoms  1681  equequ1OLD  1685  ax12dgen2  1726  sp  1747  spOLD  1748  dvelimhw  1849  ax12olem1  1927  ax10  1944  a16g  1945  cbv2h  1980  equvini  1987  equveli  1988  equsb2  2035  ax16i  2046  aecom-o  2151  ax10from10o  2177  aev-o  2182  iotaval  4350  ider  5943
  Copyright terms: Public domain W3C validator