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	⊢ 𝜑
	nic-jmaj	⊢ ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) )
Assertion	nic-mp	⊢ 𝜓

Proof

Step	Hyp	Ref	Expression
1		nic-jmin	⊢ 𝜑
2		nic-jmaj	⊢ ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) )
3		nannan	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ↔ ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) )
4	2 3	mpbi	⊢ ( 𝜑 → ( 𝜒 ∧ 𝜓 ) )
5	4	simprd	⊢ ( 𝜑 → 𝜓 )
6	1 5	ax-mp	⊢ 𝜓