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

Proof

Step	Hyp	Ref	Expression
1		nic-jmin	⊢ 𝜑
2		nic-jmaj	⊢ ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) )
3		df-nan	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ↔ ¬ ( 𝜑 ∧ ( 𝜒 ⊼ 𝜓 ) ) )
4		df-nan	⊢ ( ( 𝜒 ⊼ 𝜓 ) ↔ ¬ ( 𝜒 ∧ 𝜓 ) )
5	4	anbi2i	⊢ ( ( 𝜑 ∧ ( 𝜒 ⊼ 𝜓 ) ) ↔ ( 𝜑 ∧ ¬ ( 𝜒 ∧ 𝜓 ) ) )
6	3 5	xchbinx	⊢ ( ( 𝜑 ⊼ ( 𝜒 ⊼ 𝜓 ) ) ↔ ¬ ( 𝜑 ∧ ¬ ( 𝜒 ∧ 𝜓 ) ) )
7	2 6	mpbi	⊢ ¬ ( 𝜑 ∧ ¬ ( 𝜒 ∧ 𝜓 ) )
8		iman	⊢ ( ( 𝜑 → ( 𝜒 ∧ 𝜓 ) ) ↔ ¬ ( 𝜑 ∧ ¬ ( 𝜒 ∧ 𝜓 ) ) )
9	7 8	mpbir	⊢ ( 𝜑 → ( 𝜒 ∧ 𝜓 ) )
10	9	simprd	⊢ ( 𝜑 → 𝜓 )
11	1 10	ax-mp	⊢ 𝜓