Metamath Proof Explorer

Theorem nic-id

Description: Theorem id expressed with -/\ . (Contributed by Jeff Hoffman, 17-Nov-2007) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion nic-id ⊢ τ ⊼ τ ⊼ τ

Proof

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