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

Theorem tbwlem5 1474
 Description: Used to rederive the Lukasiewicz axioms from Tarski-Bernays-Wajsberg'. (Contributed by Anthony Hart, 16-Aug-2011.) (Proof modification is discouraged.) (New usage is discouraged.)
Assertion
Ref Expression
tbwlem5 (((φ → (ψ → ⊥ )) → ⊥ ) → φ)

Proof of Theorem tbwlem5
StepHypRef Expression
1 tbw-ax2 1466 . . . 4 (φ → (ψφ))
2 tbw-ax1 1465 . . . 4 ((ψφ) → ((φ → ⊥ ) → (ψ → ⊥ )))
31, 2tbwsyl 1469 . . 3 (φ → ((φ → ⊥ ) → (ψ → ⊥ )))
4 tbwlem1 1470 . . 3 ((φ → ((φ → ⊥ ) → (ψ → ⊥ ))) → ((φ → ⊥ ) → (φ → (ψ → ⊥ ))))
53, 4ax-mp 5 . 2 ((φ → ⊥ ) → (φ → (ψ → ⊥ )))
6 tbwlem4 1473 . 2 (((φ → ⊥ ) → (φ → (ψ → ⊥ ))) → (((φ → (ψ → ⊥ )) → ⊥ ) → φ))
75, 6ax-mp 5 1 (((φ → (ψ → ⊥ )) → ⊥ ) → φ)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ⊥ wfal 1317 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-tru 1319  df-fal 1320 This theorem is referenced by:  re1luk3  1477
 Copyright terms: Public domain W3C validator