nic-mp Show Code edit
# Derive Nicod's rule of modus ponens using 'nand', from the standard
# one. Although the major and minor premise together also imply #ch#,
# this form is necessary for useful derivations from [[nic-ax]]. In a
# pure (standalone) treatment of Nicod's axiom, this theorem would be
# changed to an axiom ($a statement). (Contributed by Jeff Hoffman,
# 19-Nov-2007.)
thm (nic-mp () (nic-jmin ph nic-jmaj (-/\ ph (-/\ ch ps))) ps nic-jmin nic-jmaj ph ch ps nic-justlem mpbi pm3.27d ax-mp)