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

Theorem tbwlem4 1473
 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
tbwlem4 (((φ → ⊥ ) → ψ) → ((ψ → ⊥ ) → φ))

Proof of Theorem tbwlem4
StepHypRef Expression
1 tbw-ax4 1468 . . . . 5 ( ⊥ → ⊥ )
2 tbw-ax1 1465 . . . . . 6 ((ψ → ⊥ ) → (( ⊥ → ⊥ ) → (ψ → ⊥ )))
3 tbwlem1 1470 . . . . . 6 (((ψ → ⊥ ) → (( ⊥ → ⊥ ) → (ψ → ⊥ ))) → (( ⊥ → ⊥ ) → ((ψ → ⊥ ) → (ψ → ⊥ ))))
42, 3ax-mp 5 . . . . 5 (( ⊥ → ⊥ ) → ((ψ → ⊥ ) → (ψ → ⊥ )))
51, 4ax-mp 5 . . . 4 ((ψ → ⊥ ) → (ψ → ⊥ ))
6 tbwlem1 1470 . . . 4 (((ψ → ⊥ ) → (ψ → ⊥ )) → (ψ → ((ψ → ⊥ ) → ⊥ )))
75, 6ax-mp 5 . . 3 (ψ → ((ψ → ⊥ ) → ⊥ ))
8 tbw-ax1 1465 . . . 4 (((φ → ⊥ ) → ψ) → ((ψ → ((ψ → ⊥ ) → ⊥ )) → ((φ → ⊥ ) → ((ψ → ⊥ ) → ⊥ ))))
9 tbwlem1 1470 . . . 4 ((((φ → ⊥ ) → ψ) → ((ψ → ((ψ → ⊥ ) → ⊥ )) → ((φ → ⊥ ) → ((ψ → ⊥ ) → ⊥ )))) → ((ψ → ((ψ → ⊥ ) → ⊥ )) → (((φ → ⊥ ) → ψ) → ((φ → ⊥ ) → ((ψ → ⊥ ) → ⊥ )))))
108, 9ax-mp 5 . . 3 ((ψ → ((ψ → ⊥ ) → ⊥ )) → (((φ → ⊥ ) → ψ) → ((φ → ⊥ ) → ((ψ → ⊥ ) → ⊥ ))))
117, 10ax-mp 5 . 2 (((φ → ⊥ ) → ψ) → ((φ → ⊥ ) → ((ψ → ⊥ ) → ⊥ )))
12 tbwlem2 1471 . . 3 (((φ → ⊥ ) → ((ψ → ⊥ ) → ⊥ )) → ((((φ → ⊥ ) → φ) → φ) → ((ψ → ⊥ ) → φ)))
13 tbwlem3 1472 . . 3 (((((φ → ⊥ ) → φ) → φ) → ((ψ → ⊥ ) → φ)) → ((ψ → ⊥ ) → φ))
1412, 13tbwsyl 1469 . 2 (((φ → ⊥ ) → ((ψ → ⊥ ) → ⊥ )) → ((ψ → ⊥ ) → φ))
1511, 14tbwsyl 1469 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:  tbwlem5  1474  re1luk2  1476
 Copyright terms: Public domain W3C validator