Theorem nic-mpALT

Description: A direct proof of nic-mp . (Contributed by NM, 30-Dec-2008) (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-mpALT	$$⊢\psi$$

Proof

Step	Hyp	Ref	Expression
1		nic-jmin	$$⊢\phi$$
2		nic-jmaj	$$⊢\left(\phi ⊼\left(\chi ⊼\psi \right)\right)$$
3		df-nan	$$⊢\left(\phi ⊼\left(\chi ⊼\psi \right)\right)\leftrightarrow \neg \left(\phi \wedge \left(\chi ⊼\psi \right)\right)$$
4		df-nan	$$⊢\left(\chi ⊼\psi \right)\leftrightarrow \neg \left(\chi \wedge \psi \right)$$
5	4	anbi2i	$$⊢\left(\phi \wedge \left(\chi ⊼\psi \right)\right)\leftrightarrow \left(\phi \wedge \neg \left(\chi \wedge \psi \right)\right)$$
6	3 5	xchbinx	$$⊢\left(\phi ⊼\left(\chi ⊼\psi \right)\right)\leftrightarrow \neg \left(\phi \wedge \neg \left(\chi \wedge \psi \right)\right)$$
7	2 6	mpbi	$$⊢\neg \left(\phi \wedge \neg \left(\chi \wedge \psi \right)\right)$$
8		iman	$$⊢\left(\phi \to \left(\chi \wedge \psi \right)\right)\leftrightarrow \neg \left(\phi \wedge \neg \left(\chi \wedge \psi \right)\right)$$
9	7 8	mpbir	$$⊢\phi \to \left(\chi \wedge \psi \right)$$
10	9	simprd	$$⊢\phi \to \psi$$
11	1 10	ax-mp	$$⊢\psi$$