Metamath Proof Explorer

Theorem nic-idlem2

Description: Lemma for nic-id . Inference used by nic-id . (Contributed by Jeff Hoffman, 17-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Hypothesis nic-idlem2.1 ⊢ η ⊼ φ ⊼ χ ⊼ ψ ⊼ θ
Assertion nic-idlem2 ⊢ θ ⊼ τ ⊼ τ ⊼ τ ⊼ η

Proof

Step Hyp Ref Expression
1 nic-idlem2.1 ⊢ η ⊼ φ ⊼ χ ⊼ ψ ⊼ θ
2 nic-ax ⊢ φ ⊼ χ ⊼ ψ ⊼ τ ⊼ τ ⊼ τ ⊼ φ ⊼ χ ⊼ φ ⊼ φ ⊼ φ ⊼ φ
3 2 nic-imp ⊢ θ ⊼ τ ⊼ τ ⊼ τ ⊼ φ ⊼ χ ⊼ ψ ⊼ θ ⊼ φ ⊼ χ ⊼ ψ ⊼ θ
4 3 nic-imp ⊢ η ⊼ φ ⊼ χ ⊼ ψ ⊼ θ ⊼ θ ⊼ τ ⊼ τ ⊼ τ ⊼ η ⊼ θ ⊼ τ ⊼ τ ⊼ τ ⊼ η
5 1 4 nic-mp ⊢ θ ⊼ τ ⊼ τ ⊼ τ ⊼ η