Metamath Proof Explorer

Theorem nic-luk3

Description: Proof of luk-3 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-luk3 ⊢ φ → ¬ φ → ψ

Proof

Step Hyp Ref Expression
1 nic-dfim ⊢ ¬ φ ⊼ ψ ⊼ ψ ⊼ ¬ φ → ψ ⊼ ¬ φ ⊼ ψ ⊼ ψ ⊼ ¬ φ ⊼ ψ ⊼ ψ ⊼ ¬ φ → ψ ⊼ ¬ φ → ψ
2 1 nic-bi1 ⊢ ¬ φ ⊼ ψ ⊼ ψ ⊼ ¬ φ → ψ ⊼ ¬ φ → ψ
3 nic-dfneg ⊢ φ ⊼ φ ⊼ ¬ φ ⊼ φ ⊼ φ ⊼ φ ⊼ φ ⊼ ¬ φ ⊼ ¬ φ
4 3 nic-bi2 ⊢ ¬ φ ⊼ φ ⊼ φ ⊼ φ ⊼ φ
5 nic-id ⊢ φ ⊼ φ ⊼ φ
6 4 5 nic-iimp1 ⊢ φ ⊼ ¬ φ
7 2 6 nic-iimp2 ⊢ φ ⊼ ¬ φ → ψ ⊼ ¬ φ → ψ
8 nic-dfim ⊢ φ ⊼ ¬ φ → ψ ⊼ ¬ φ → ψ ⊼ φ → ¬ φ → ψ ⊼ φ ⊼ ¬ φ → ψ ⊼ ¬ φ → ψ ⊼ φ ⊼ ¬ φ → ψ ⊼ ¬ φ → ψ ⊼ φ → ¬ φ → ψ ⊼ φ → ¬ φ → ψ
9 8 nic-bi1 ⊢ φ ⊼ ¬ φ → ψ ⊼ ¬ φ → ψ ⊼ φ → ¬ φ → ψ ⊼ φ → ¬ φ → ψ
10 7 9 nic-mp ⊢ φ → ¬ φ → ψ