Theorem nic-mp

Description: 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) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nic-jmin	|- ph
	nic-jmaj	|- ( ph -/\ ( ch -/\ ps ) )
Assertion	nic-mp	|- ps

Proof

Step	Hyp	Ref	Expression
1		nic-jmin	|- ph
2		nic-jmaj	|- ( ph -/\ ( ch -/\ ps ) )
3		nannan	|- ( ( ph -/\ ( ch -/\ ps ) ) <-> ( ph -> ( ch /\ ps ) ) )
4	2 3	mpbi	|- ( ph -> ( ch /\ ps ) )
5	4	simprd	|- ( ph -> ps )
6	1 5	ax-mp	|- ps