Metamath Proof Explorer

Theorem nic-luk2

Description: Proof of luk-2 from nic-ax and nic-mp . (Contributed by Jeff Hoffman, 18-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

		Ref	Expression
	Assertion	nic-luk2	$⊢ (\neg φ \to φ) \to φ$

Proof

Step	Hyp	Ref	Expression
1		nic-dfim	$⊢ (((\neg φ ⊼ (φ ⊼ φ)) ⊼ (\neg φ \to φ)) ⊼ (((\neg φ ⊼ (φ ⊼ φ)) ⊼ (\neg φ ⊼ (φ ⊼ φ))) ⊼ ((\neg φ \to φ) ⊼ (\neg φ \to φ))))$
2	1	nic-bi2	$⊢ ((\neg φ \to φ) ⊼ ((\neg φ ⊼ (φ ⊼ φ)) ⊼ (\neg φ ⊼ (φ ⊼ φ))))$
3		nic-dfneg	$⊢ (((φ ⊼ φ) ⊼ \neg φ) ⊼ (((φ ⊼ φ) ⊼ (φ ⊼ φ)) ⊼ (\neg φ ⊼ \neg φ)))$
4		nic-id	$⊢ ((φ ⊼ φ) ⊼ ((φ ⊼ φ) ⊼ (φ ⊼ φ)))$
5	3 4	nic-iimp1	$⊢ ((φ ⊼ φ) ⊼ ((φ ⊼ φ) ⊼ \neg φ))$
6	5	nic-isw2	$⊢ ((φ ⊼ φ) ⊼ (\neg φ ⊼ (φ ⊼ φ)))$
7	2 6	nic-iimp1	$⊢ ((φ ⊼ φ) ⊼ (\neg φ \to φ))$
8	7	nic-isw1	$⊢ ((\neg φ \to φ) ⊼ (φ ⊼ φ))$
9		nic-dfim	$⊢ ((((\neg φ \to φ) ⊼ (φ ⊼ φ)) ⊼ ((\neg φ \to φ) \to φ)) ⊼ ((((\neg φ \to φ) ⊼ (φ ⊼ φ)) ⊼ ((\neg φ \to φ) ⊼ (φ ⊼ φ))) ⊼ (((\neg φ \to φ) \to φ) ⊼ ((\neg φ \to φ) \to φ))))$
10	9	nic-bi1	$⊢ (((\neg φ \to φ) ⊼ (φ ⊼ φ)) ⊼ (((\neg φ \to φ) \to φ) ⊼ ((\neg φ \to φ) \to φ)))$
11	8 10	nic-mp	$⊢ (\neg φ \to φ) \to φ$