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	$$⊢\phi$$
	nic-smaj	$$⊢\phi \to \psi$$
Assertion	nic-stdmp	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		nic-smin	$$⊢\phi$$
2		nic-smaj	$$⊢\phi \to \psi$$
3		nic-dfim	$$⊢\left(\left(\left(\phi ⊼\left(\psi ⊼\psi \right)\right)⊼\left(\phi \to \psi \right)\right)⊼\left(\left(\left(\phi ⊼\left(\psi ⊼\psi \right)\right)⊼\left(\phi ⊼\left(\psi ⊼\psi \right)\right)\right)⊼\left(\left(\phi \to \psi \right)⊼\left(\phi \to \psi \right)\right)\right)\right)$$
4	3	nic-bi2	$$⊢\left(\left(\phi \to \psi \right)⊼\left(\left(\phi ⊼\left(\psi ⊼\psi \right)\right)⊼\left(\phi ⊼\left(\psi ⊼\psi \right)\right)\right)\right)$$
5	2 4	nic-mp	$$⊢\left(\phi ⊼\left(\psi ⊼\psi \right)\right)$$
6	1 5	nic-mp	$$⊢\psi$$