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 ⊢τ⊼τ⊼τ