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	$$⊢\phi$$
	nic-jmaj	$$⊢\left(\phi ⊼\left(\chi ⊼\psi \right)\right)$$
Assertion	nic-mp	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		nic-jmin	$$⊢\phi$$
2		nic-jmaj	$$⊢\left(\phi ⊼\left(\chi ⊼\psi \right)\right)$$
3		nannan	$$⊢\left(\phi ⊼\left(\chi ⊼\psi \right)\right)\leftrightarrow \left(\phi \to \left(\chi \wedge \psi \right)\right)$$
4	2 3	mpbi	$$⊢\phi \to \left(\chi \wedge \psi \right)$$
5	4	simprd	$$⊢\phi \to \psi$$
6	1 5	ax-mp	$$⊢\psi$$