MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  equcomi Structured version   Unicode version

Theorem equcomi 1691
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  =  y  ->  y  =  x )

Proof of Theorem equcomi
StepHypRef Expression
1 equid 1688 . 2  |-  x  =  x
2 ax-8 1687 . 2  |-  ( x  =  y  ->  (
x  =  x  -> 
y  =  x ) )
31, 2mpi 17 1  |-  ( x  =  y  ->  y  =  x )
Colors of variables: wff set class
Syntax hints:    -> wi 4
This theorem is referenced by:  equcom  1692  equcoms  1693  equequ1OLD  1697  ax12dgen2  1741  spOLD  1764  dvelimhwOLD  1877  cbv2h  1979  ax12olem1  2005  ax12olem1OLD  2011  ax10  2025  ax10OLD  2032  a16gOLD  2049  ax16i  2051  equvini  2083  equviniOLD  2084  equveliOLD  2086  equsb2  2102  aecom-o  2228  ax10from10o  2254  aev-o  2259  axsep  4329  rext  4412  iotaval  5429  soxp  6459  axextnd  8466  prodmo  25262  finminlem  26321  dvelimhwNEW7  29455  ax10NEW7  29473  cbv2hwAUX7  29513  equviniNEW7  29527  equveliNEW7  29528  equsb2NEW7  29539  a16gNEW7  29546  ax16iNEW7  29551  ax7w3AUX7  29651  ax7w9AUX7  29660  alcomw9bAUX7  29661  cbv2hOLD7  29721
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687
This theorem depends on definitions:  df-bi 178  df-ex 1551
  Copyright terms: Public domain W3C validator