Theorem lukshefth2 1461

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

Assertion

Ref	Expression
lukshefth2	⊢ ((τ ⊼ θ) ⊼ ((θ ⊼ τ) ⊼ (θ ⊼ τ)))

Proof of Theorem lukshefth2

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

This proof depends on syntax axioms:   ⊼ wnan 1287

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 177  df-an 360  df-nan 1288

This theorem is used by:  renicax  1462