Metamath Proof Explorer

Theorem nic-idlem1

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

Ref Expression
Assertion nic-idlem1 ⊢ θ ⊼ τ ⊼ τ ⊼ τ ⊼ φ ⊼ χ ⊼ ψ ⊼ θ ⊼ φ ⊼ χ ⊼ ψ ⊼ θ

Proof

Step Hyp Ref Expression
1 nic-ax ⊢ φ ⊼ χ ⊼ ψ ⊼ τ ⊼ τ ⊼ τ ⊼ φ ⊼ χ ⊼ φ ⊼ φ ⊼ φ ⊼ φ
2 1 nic-imp ⊢ θ ⊼ τ ⊼ τ ⊼ τ ⊼ φ ⊼ χ ⊼ ψ ⊼ θ ⊼ φ ⊼ χ ⊼ ψ ⊼ θ