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	|- ph
	nic-jmaj	|- ( ph -/\ ( ch -/\ ps ) )
Assertion	nic-mpALT	|- ps

Proof

Step	Hyp	Ref	Expression
1		nic-jmin	|- ph
2		nic-jmaj	|- ( ph -/\ ( ch -/\ ps ) )
3		df-nan	|- ( ( ph -/\ ( ch -/\ ps ) ) <-> -. ( ph /\ ( ch -/\ ps ) ) )
4		df-nan	|- ( ( ch -/\ ps ) <-> -. ( ch /\ ps ) )
5	4	anbi2i	|- ( ( ph /\ ( ch -/\ ps ) ) <-> ( ph /\ -. ( ch /\ ps ) ) )
6	3 5	xchbinx	|- ( ( ph -/\ ( ch -/\ ps ) ) <-> -. ( ph /\ -. ( ch /\ ps ) ) )
7	2 6	mpbi	|- -. ( ph /\ -. ( ch /\ ps ) )
8		iman	|- ( ( ph -> ( ch /\ ps ) ) <-> -. ( ph /\ -. ( ch /\ ps ) ) )
9	7 8	mpbir	|- ( ph -> ( ch /\ ps ) )
10	9	simprd	|- ( ph -> ps )
11	1 10	ax-mp	|- ps