Metamath Proof Explorer

Theorem lukshefth1

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

		Ref	Expression
	Assertion	lukshefth1	$⊢ ((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (θ ⊼ (θ ⊼ θ))) ⊼ (φ ⊼ (ψ ⊼ χ)))$

Proof

Step	Hyp	Ref	Expression
1		lukshef-ax1	$⊢ ((φ ⊼ (ψ ⊼ χ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ)))))$
2		lukshef-ax1	$⊢ ((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ (θ ⊼ θ)) ⊼ ((θ ⊼ τ) ⊼ ((τ ⊼ θ) ⊼ (τ ⊼ θ)))))$
3		lukshef-ax1	$⊢ (((τ ⊼ (τ ⊼ τ)) ⊼ ((θ ⊼ (θ ⊼ θ)) ⊼ ((θ ⊼ τ) ⊼ ((τ ⊼ θ) ⊼ (τ ⊼ θ))))) ⊼ ((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ ((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))))) ⊼ ((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (θ ⊼ (θ ⊼ θ))) ⊼ (((τ ⊼ (τ ⊼ τ)) ⊼ ((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ)))) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))))))))$
4	2 3	nic-mp	$⊢ ((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (θ ⊼ (θ ⊼ θ))) ⊼ (((τ ⊼ (τ ⊼ τ)) ⊼ ((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ)))) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))))))$
5		lukshef-ax1	$⊢ (((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (θ ⊼ (θ ⊼ θ))) ⊼ (((τ ⊼ (τ ⊼ τ)) ⊼ ((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ)))) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ)))))) ⊼ (((φ ⊼ (ψ ⊼ χ)) ⊼ ((φ ⊼ (ψ ⊼ χ)) ⊼ (φ ⊼ (ψ ⊼ χ)))) ⊼ (((φ ⊼ (ψ ⊼ χ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))))) ⊼ (((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (θ ⊼ (θ ⊼ θ))) ⊼ (φ ⊼ (ψ ⊼ χ))) ⊼ ((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (θ ⊼ (θ ⊼ θ))) ⊼ (φ ⊼ (ψ ⊼ χ)))))))$
6	4 5	nic-mp	$⊢ (((φ ⊼ (ψ ⊼ χ)) ⊼ ((τ ⊼ (τ ⊼ τ)) ⊼ ((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))))) ⊼ (((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (θ ⊼ (θ ⊼ θ))) ⊼ (φ ⊼ (ψ ⊼ χ))) ⊼ ((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (θ ⊼ (θ ⊼ θ))) ⊼ (φ ⊼ (ψ ⊼ χ)))))$
7	1 6	nic-mp	$⊢ ((((τ ⊼ ψ) ⊼ ((φ ⊼ τ) ⊼ (φ ⊼ τ))) ⊼ (θ ⊼ (θ ⊼ θ))) ⊼ (φ ⊼ (ψ ⊼ χ)))$