NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  lukshefth2 GIF version

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
StepHypRef Expression
1 lukshef-ax1 1459 . . . 4 ((ψ (χ φ)) ((θ (θ θ)) ((θ χ) ((ψ θ) (ψ θ)))))
2 lukshef-ax1 1459 . . . 4 (((ψ (χ φ)) ((θ (θ θ)) ((θ χ) ((ψ θ) (ψ θ))))) ((θ (θ θ)) ((θ (θ (θ θ))) (((ψ (χ φ)) θ) ((ψ (χ φ)) θ)))))
31, 2nic-mp 1436 . . 3 ((θ (θ (θ θ))) (((ψ (χ φ)) θ) ((ψ (χ φ)) θ)))
4 lukshefth1 1460 . . . 4 ((((τ φ) ((φ τ) (φ τ))) (θ (θ θ))) (φ (φ φ)))
5 lukshef-ax1 1459 . . . . 5 (((θ (θ (θ θ))) (((ψ (χ φ)) θ) ((ψ (χ φ)) θ))) ((φ (φ φ)) ((φ ((ψ (χ φ)) θ)) (((θ (θ (θ θ))) φ) ((θ (θ (θ θ))) φ)))))
6 lukshef-ax1 1459 . . . . 5 ((((θ (θ (θ θ))) (((ψ (χ φ)) θ) ((ψ (χ φ)) θ))) ((φ (φ φ)) ((φ ((ψ (χ φ)) θ)) (((θ (θ (θ θ))) φ) ((θ (θ (θ θ))) φ))))) (((((τ φ) ((φ τ) (φ τ))) (θ (θ θ))) ((((τ φ) ((φ τ) (φ τ))) (θ (θ θ))) (((τ φ) ((φ τ) (φ τ))) (θ (θ θ))))) (((((τ φ) ((φ τ) (φ τ))) (θ (θ θ))) (φ (φ φ))) ((((θ (θ (θ θ))) (((ψ (χ φ)) θ) ((ψ (χ φ)) θ))) (((τ φ) ((φ τ) (φ τ))) (θ (θ θ)))) (((θ (θ (θ θ))) (((ψ (χ φ)) θ) ((ψ (χ φ)) θ))) (((τ φ) ((φ τ) (φ τ))) (θ (θ θ))))))))
75, 6nic-mp 1436 . . . 4 (((((τ φ) ((φ τ) (φ τ))) (θ (θ θ))) (φ (φ φ))) ((((θ (θ (θ θ))) (((ψ (χ φ)) θ) ((ψ (χ φ)) θ))) (((τ φ) ((φ τ) (φ τ))) (θ (θ θ)))) (((θ (θ (θ θ))) (((ψ (χ φ)) θ) ((ψ (χ φ)) θ))) (((τ φ) ((φ τ) (φ τ))) (θ (θ θ))))))
84, 7nic-mp 1436 . . 3 (((θ (θ (θ θ))) (((ψ (χ φ)) θ) ((ψ (χ φ)) θ))) (((τ φ) ((φ τ) (φ τ))) (θ (θ θ))))
93, 8nic-mp 1436 . 2 (θ (θ θ))
10 lukshef-ax1 1459 . 2 ((θ (θ θ)) ((τ (τ τ)) ((τ θ) ((θ τ) (θ τ)))))
119, 10nic-mp 1436 1 ((τ θ) ((θ τ) (θ τ)))
Colors of variables: wff setvar class
Syntax hints:   wnan 1287
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8
This theorem depends on definitions:  df-bi 177  df-an 360  df-nan 1288
This theorem is referenced by:  renicax  1462
  Copyright terms: Public domain W3C validator