Theorem nic-stdmp

Description: Derive the standard modus ponens from nic-mp . (Contributed by Jeff Hoffman, 18-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nic-smin	⊢ 𝜑
	nic-smaj	⊢ ( 𝜑 → 𝜓 )
Assertion	nic-stdmp	⊢ 𝜓

Proof

Step	Hyp	Ref	Expression
1		nic-smin	⊢ 𝜑
2		nic-smaj	⊢ ( 𝜑 → 𝜓 )
3		nic-dfim	⊢ ( ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜓 ) ) ⊼ ( 𝜑 → 𝜓 ) ) ⊼ ( ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜓 ) ) ⊼ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜓 ) ) ) ⊼ ( ( 𝜑 → 𝜓 ) ⊼ ( 𝜑 → 𝜓 ) ) ) )
4	3	nic-bi2	⊢ ( ( 𝜑 → 𝜓 ) ⊼ ( ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜓 ) ) ⊼ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜓 ) ) ) )
5	2 4	nic-mp	⊢ ( 𝜑 ⊼ ( 𝜓 ⊼ 𝜓 ) )
6	1 5	nic-mp	⊢ 𝜓