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

Theorem equcomi 1687
 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

Proof of Theorem equcomi
StepHypRef Expression
1 equid 1684 . 2
2 ax-8 1683 . 2
31, 2mpi 17 1
 Colors of variables: wff set class Syntax hints:   wi 4 This theorem is referenced by:  equcom  1688  equcoms  1689  equequ1OLD  1693  ax12dgen2  1737  spOLD  1760  dvelimhwOLD  1873  ax12olem1  1972  ax12olem1OLD  1977  ax10  1991  ax10OLD  1998  a16gOLD  2013  cbv2h  2033  equvini  2040  equveli  2041  equsb2  2082  ax16i  2093  aecom-o  2199  ax10from10o  2225  aev-o  2230  axsep  4284  rext  4367  iotaval  5383  soxp  6409  axextnd  8413  prodmo  25055  finminlem  26028  dvelimhwNEW7  28809  ax10NEW7  28827  cbv2hwAUX7  28867  equviniNEW7  28879  equveliNEW7  28880  equsb2NEW7  28891  a16gNEW7  28898  ax16iNEW7  28903  ax7w3AUX7  28999  ax7w9AUX7  29008  alcomw9bAUX7  29009  cbv2hOLD7  29053 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683 This theorem depends on definitions:  df-bi 178  df-ex 1548
 Copyright terms: Public domain W3C validator