<gh_stars>0
{
  "citations" : [ {
    "textCitation" : "[See pm2.01d on Metamath](http://us.metamath.org/mpegif/pm2.01d.html)"
  } ],
  "names" : [ "pm2.01d" ],
  "language" : "METAMATH_SET_MM",
  "lookupTerms" : [ "#T_wph", "#T_wi", "#T_wps", "#T_wi", "#T_wn", "#T_wps", "#T_wph", "#T_wi", "#T_wn", "#T_wps" ],
  "metaLanguage" : "METAMATH",
  "remarks" : " Deduction based on reductio ad absurdum.  (Contributed by NM, 18-Aug-1993.)  (Proof shortened by <NAME>, 5-Mar-2013.) \n\n---\n\n Deduction based on reductio ad absurdum.  (Contributed by NM, 18-Aug-1993.)  (Revised by <NAME>, 31-Jan-2015.) ",
  "statement" : "pm2.01d.1 $e |- ( ph -> ( ps -> -. ps ) ) $.\npm2.01d $p |- ( ph -> -. ps ) $."
}