Metamath Proof Explorer

Theorem renicax

Description: A rederivation of nic-ax from lukshef-ax1 , proving that lukshef-ax1 with nic-mp can be used as a complete axiomatization of propositional calculus. (Contributed by Anthony Hart, 31-Jul-2011) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion renicax ⊢ φ ⊼ χ ⊼ ψ ⊼ τ ⊼ τ ⊼ τ ⊼ θ ⊼ χ ⊼ φ ⊼ θ ⊼ φ ⊼ θ

Proof

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