<reponame>Sophize/set_mm
{
  "citations" : [ {
    "textCitation" : "[See eqeqan12d on Metamath](http://us.metamath.org/mpegif/eqeqan12d.html)"
  } ],
  "names" : [ "eqeqan12d" ],
  "language" : "METAMATH_SET_MM",
  "lookupTerms" : [ "#T_wph", "#T_wi", "#T_cA", "#T_wceq", "#T_cB", "#T_wps", "#T_wi", "#T_cC", "#T_wceq", "#T_cD", "#T_wph", "#T_wa", "#T_wps", "#T_wi", "#T_cA", "#T_wceq", "#T_cC", "#T_wb", "#T_cB", "#T_wceq", "#T_cD" ],
  "metaLanguage" : "METAMATH",
  "remarks" : " A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)  (Proof shortened by <NAME>, 25-May-2011.)  (Proof shortened by <NAME>, 20-Nov-2019.) \n\n---\n\n A useful inference for substituting definitions into an equality. (Contributed by NM, 9-Aug-1994.)  (Proof shortened by <NAME>, 25-May-2011.) ",
  "statement" : "eqeqan12d.1 $e |- ( ph -> A = B ) $.\neqeqan12d.2 $e |- ( ps -> C = D ) $.\neqeqan12d $p |- ( ( ph /\\ ps ) -> ( A = C <-> B = D ) ) $."
}