nic-stdmp Show Code edit
# Derive the standard modus ponens from [[nic-mp]]. (Contributed by Jeff
# Hoffman, 18-Nov-2007.)
thm (nic-stdmp () (nic-smin ph nic-smaj (-> ph ps)) ps nic-smin nic-smaj ph ps nic-dfim nic-bi2 nic-mp nic-mp)
ps
edit