Metamath Proof Explorer

Theorem lukshefth2

Description: Lemma for renicax . (Contributed by NM, 31-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion lukshefth2 ⊢ τ ⊼ θ ⊼ θ ⊼ τ ⊼ θ ⊼ τ

Proof

Step Hyp Ref Expression
1 lukshef-ax1 ⊢ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ χ ⊼ ψ ⊼ θ ⊼ ψ ⊼ θ
2 lukshef-ax1 ⊢ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ χ ⊼ ψ ⊼ θ ⊼ ψ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ
3 1 2 nic-mp ⊢ θ ⊼ θ ⊼ θ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ
4 lukshefth1 ⊢ τ ⊼ φ ⊼ φ ⊼ τ ⊼ φ ⊼ τ ⊼ θ ⊼ θ ⊼ θ ⊼ φ ⊼ φ ⊼ φ
5 lukshef-ax1 ⊢ θ ⊼ θ ⊼ θ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ φ ⊼ φ ⊼ φ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ φ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ φ
6 lukshef-ax1 ⊢ θ ⊼ θ ⊼ θ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ φ ⊼ φ ⊼ φ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ φ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ φ ⊼ τ ⊼ φ ⊼ φ ⊼ τ ⊼ φ ⊼ τ ⊼ θ ⊼ θ ⊼ θ ⊼ τ ⊼ φ ⊼ φ ⊼ τ ⊼ φ ⊼ τ ⊼ θ ⊼ θ ⊼ θ ⊼ τ ⊼ φ ⊼ φ ⊼ τ ⊼ φ ⊼ τ ⊼ θ ⊼ θ ⊼ θ ⊼ τ ⊼ φ ⊼ φ ⊼ τ ⊼ φ ⊼ τ ⊼ θ ⊼ θ ⊼ θ ⊼ φ ⊼ φ ⊼ φ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ τ ⊼ φ ⊼ φ ⊼ τ ⊼ φ ⊼ τ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ τ ⊼ φ ⊼ φ ⊼ τ ⊼ φ ⊼ τ ⊼ θ ⊼ θ ⊼ θ
7 5 6 nic-mp ⊢ τ ⊼ φ ⊼ φ ⊼ τ ⊼ φ ⊼ τ ⊼ θ ⊼ θ ⊼ θ ⊼ φ ⊼ φ ⊼ φ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ τ ⊼ φ ⊼ φ ⊼ τ ⊼ φ ⊼ τ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ τ ⊼ φ ⊼ φ ⊼ τ ⊼ φ ⊼ τ ⊼ θ ⊼ θ ⊼ θ
8 4 7 nic-mp ⊢ θ ⊼ θ ⊼ θ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ ψ ⊼ χ ⊼ φ ⊼ θ ⊼ τ ⊼ φ ⊼ φ ⊼ τ ⊼ φ ⊼ τ ⊼ θ ⊼ θ ⊼ θ
9 3 8 nic-mp ⊢ θ ⊼ θ ⊼ θ
10 lukshef-ax1 ⊢ θ ⊼ θ ⊼ θ ⊼ τ ⊼ τ ⊼ τ ⊼ τ ⊼ θ ⊼ θ ⊼ τ ⊼ θ ⊼ τ
11 9 10 nic-mp ⊢ τ ⊼ θ ⊼ θ ⊼ τ ⊼ θ ⊼ τ