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

Theorem re1luk2 1476
 Description: luk-2 1421 derived from the Tarski-Bernays-Wajsberg axioms. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
re1luk2 ((¬ φφ) → φ)

Proof of Theorem re1luk2
StepHypRef Expression
1 tbw-negdf 1464 . . . 4 (((¬ φ → (φ → ⊥ )) → (((φ → ⊥ ) → ¬ φ) → ⊥ )) → ⊥ )
2 tbw-ax2 1466 . . . . 5 ((((φ → ⊥ ) → ¬ φ) → ⊥ ) → ((¬ φ → (φ → ⊥ )) → (((φ → ⊥ ) → ¬ φ) → ⊥ )))
3 tbwlem4 1473 . . . . 5 (((((φ → ⊥ ) → ¬ φ) → ⊥ ) → ((¬ φ → (φ → ⊥ )) → (((φ → ⊥ ) → ¬ φ) → ⊥ ))) → ((((¬ φ → (φ → ⊥ )) → (((φ → ⊥ ) → ¬ φ) → ⊥ )) → ⊥ ) → ((φ → ⊥ ) → ¬ φ)))
42, 3ax-mp 8 . . . 4 ((((¬ φ → (φ → ⊥ )) → (((φ → ⊥ ) → ¬ φ) → ⊥ )) → ⊥ ) → ((φ → ⊥ ) → ¬ φ))
51, 4ax-mp 8 . . 3 ((φ → ⊥ ) → ¬ φ)
6 tbw-ax1 1465 . . 3 (((φ → ⊥ ) → ¬ φ) → ((¬ φφ) → ((φ → ⊥ ) → φ)))
75, 6ax-mp 8 . 2 ((¬ φφ) → ((φ → ⊥ ) → φ))
8 tbw-ax3 1467 . 2 (((φ → ⊥ ) → φ) → φ)
97, 8tbwsyl 1469 1 ((¬ φφ) → φ)
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ⊥ wfal 1317 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8 This theorem depends on definitions:  df-bi 177  df-tru 1319  df-fal 1320 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator